let A be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF A holds (p => q) => ((q => r) => (p => r)) in TAUT A

let p, q, r be Element of CQC-WFF A; :: thesis: (p => q) => ((q => r) => (p => r)) in TAUT A

(p => q) => (('not' (q '&' ('not' r))) => ('not' (p '&' ('not' r)))) in TAUT A by CQC_THE1:44;

then (p => q) => ((q => r) => ('not' (p '&' ('not' r)))) in TAUT A by QC_LANG2:def 2;

hence (p => q) => ((q => r) => (p => r)) in TAUT A by QC_LANG2:def 2; :: thesis: verum

let p, q, r be Element of CQC-WFF A; :: thesis: (p => q) => ((q => r) => (p => r)) in TAUT A

(p => q) => (('not' (q '&' ('not' r))) => ('not' (p '&' ('not' r)))) in TAUT A by CQC_THE1:44;

then (p => q) => ((q => r) => ('not' (p '&' ('not' r)))) in TAUT A by QC_LANG2:def 2;

hence (p => q) => ((q => r) => (p => r)) in TAUT A by QC_LANG2:def 2; :: thesis: verum