theorem :: PROCAL_1:34

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