let p, q, s be Element of MC-wff ; :: thesis: ( s => (q => p) in IPC-Taut & q in IPC-Taut implies s => p in IPC-Taut )
assume that
A1: s => (q => p) in IPC-Taut and
A2: q in IPC-Taut ; :: thesis: s => p in IPC-Taut
(s => (q => p)) => (q => (s => p)) in IPC-Taut by Th29;
then q => (s => p) in IPC-Taut by A1, Def14;
hence s => p in IPC-Taut by A2, Def14; :: thesis: verum