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