theorem Th40: :: PROCAL_1:40

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