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