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