let p, q, r be Element of CQC-WFF ; :: thesis: (p => q) => ((q => r) => (p => r)) in TAUT
(p => q) => (('not' (q '&' ('not' r))) => ('not' (p '&' ('not' r)))) in TAUT by CQC_THE1:44;
then (p => q) => ((q => r) => ('not' (p '&' ('not' r)))) in TAUT by QC_LANG2:def 2;
hence (p => q) => ((q => r) => (p => r)) in TAUT by QC_LANG2:def 2; :: thesis: verum