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