let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A holds ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A
let p, q, r be Element of CQC-WFF A; :: thesis: ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A
(('not' p) => q) => ((('not' p) => r) => (('not' p) => (q '&' r))) in TAUT A by Th33;
then (p 'or' q) => ((('not' p) => r) => (('not' p) => (q '&' r))) in TAUT A by Lm1;
then (p 'or' q) => ((p 'or' r) => (('not' p) => (q '&' r))) in TAUT A by Lm1;
then A1: (p 'or' q) => ((p 'or' r) => (p 'or' (q '&' r))) in TAUT A by Lm1;
((p 'or' q) => ((p 'or' r) => (p 'or' (q '&' r)))) => (((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r))) in TAUT A by Th32;
hence ((p 'or' q) '&' (p 'or' r)) => (p 'or' (q '&' r)) in TAUT A by A1, CQC_THE1:46; :: thesis: verum