theorem Th32: :: PROCAL_1:32

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