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