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