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