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