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