let p, q be Element of MC-wff ; :: thesis: (p => (p => q)) => (p => q) in IPC-Taut
(p => (p => q)) => ((p => p) => (p => q)) in IPC-Taut by Def14;
then A1: (p => p) => ((p => (p => q)) => (p => q)) in IPC-Taut by Th23;
p => p in IPC-Taut by Th17;
hence (p => (p => q)) => (p => q) in IPC-Taut by A1, Def14; :: thesis: verum