let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A holds (p => (q => r)) => ((p '&' q) => r) in TAUT A
let p, q, r be Element of CQC-WFF A; :: thesis: (p => (q => r)) => ((p '&' q) => r) in TAUT A
A1: (p => ((p '&' q) => r)) => ((p '&' q) => (p => r)) in TAUT A by LUKASI_1:8;
((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r)) in TAUT A by LUKASI_1:11;
then A2: ((p '&' q) => (p => r)) => ((p '&' q) => r) in TAUT A by Th19, LUKASI_1:16;
( (p '&' q) => q in TAUT A & ((p '&' q) => q) => ((q => r) => ((p '&' q) => r)) in TAUT A ) by Th21, LUKASI_1:1;
then (q => r) => ((p '&' q) => r) in TAUT A by CQC_THE1:46;
then A3: p => ((q => r) => ((p '&' q) => r)) in TAUT A by LUKASI_1:13;
(p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r))) in TAUT A by LUKASI_1:11;
then (p => (q => r)) => (p => ((p '&' q) => r)) in TAUT A by A3, CQC_THE1:46;
then (p => (q => r)) => ((p '&' q) => (p => r)) in TAUT A by A1, LUKASI_1:3;
hence (p => (q => r)) => ((p '&' q) => r) in TAUT A by A2, LUKASI_1:3; :: thesis: verum