let p, q be Element of MC-wff ; :: thesis: |-_IPC (p => FALSUM) => (p => q)
A1: (FALSUM => q) => ((p => FALSUM) => (p => q)) in IPC-Taut by INTPRO_1:22;
FALSUM => q in IPC-Taut by INTPRO_1:def 14;
then (p => FALSUM) => (p => q) in IPC-Taut by A1, INTPRO_1:def 14;
hence |-_IPC (p => FALSUM) => (p => q) by Th69; :: thesis: verum