theorem Th4: :: CQC_THE2:4

for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st (p '&' q) => r is valid holds
q => (p => r) is valid