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