theorem Th36: :: PROCAL_1:36

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