let p, q, r be Element of MC-wff ; :: thesis: ((p => q) => r) => (q => r) in IPC-Taut
( q => (p => q) in IPC-Taut & (q => (p => q)) => (((p => q) => r) => (q => r)) in IPC-Taut ) by Def14, Th24;
hence ((p => q) => r) => (q => r) in IPC-Taut by Def14; :: thesis: verum