let p, q, r be Element of MC-wff ; (p => (q => r)) => ((p '&' q) => r) in IPC-Taut
A1:
((p '&' q) => q) => ((q => r) => ((p '&' q) => r)) in IPC-Taut
by Th24;
(p '&' q) => q in IPC-Taut
by Def14;
then
(q => r) => ((p '&' q) => r) in IPC-Taut
by A1, Def14;
then A2:
p => ((q => r) => ((p '&' q) => r)) in IPC-Taut
by Th18;
A3:
(p => ((p '&' q) => r)) => ((p '&' q) => (p => r)) in IPC-Taut
by Th29;
(p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r))) in IPC-Taut
by Def14;
then
(p => (q => r)) => (p => ((p '&' q) => r)) in IPC-Taut
by A2, Def14;
then A4:
(p => (q => r)) => ((p '&' q) => (p => r)) in IPC-Taut
by A3, Th26;
A5:
(p '&' q) => p in IPC-Taut
by Def14;
((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r)) in IPC-Taut
by Def14;
then
((p '&' q) => (p => r)) => ((p '&' q) => r) in IPC-Taut
by A5, Th32;
hence
(p => (q => r)) => ((p '&' q) => r) in IPC-Taut
by A4, Th26; verum