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