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