theorem Th28: :: PROCAL_1:28

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds p => (q => (p '&' q)) in TAUT A