let q, r, p be Element of CQC-WFF ; :: thesis: (q => r) => ((p => q) => (p => r)) in TAUT
( (p => q) => ((q => r) => (p => r)) in TAUT & ((p => q) => ((q => r) => (p => r))) => ((q => r) => ((p => q) => (p => r))) in TAUT ) by Th1, Th8;
hence (q => r) => ((p => q) => (p => r)) in TAUT by CQC_THE1:46; :: thesis: verum