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