let p, q, s be Element of MC-wff ; :: thesis: (p => q) => ((s '&' p) => (s '&' q)) in IPC-Taut
set P = p => q;
set Q = p '&' s;
set S = s '&' q;
set T = s '&' p;
A1: (p => q) => ((p '&' s) => (s '&' q)) in IPC-Taut by Th48;
A2: (s '&' p) => (p '&' s) in IPC-Taut by Th46;
((p => q) => ((p '&' s) => (s '&' q))) => (((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q)))) in IPC-Taut by Th27;
then ((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q))) in IPC-Taut by A1, Def14;
hence (p => q) => ((s '&' p) => (s '&' q)) in IPC-Taut by A2, Def14; :: thesis: verum