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