theorem :: PROCAL_1:38

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