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