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