theorem Th33: :: PROCAL_1:33

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