theorem :: PROCAL_1:39

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