let p, q be Element of MC-wff ; :: thesis: |-_IPC ((p => FALSUM) 'or' q) => (p => q)
A1: (p => FALSUM) => (p => q) in IPC-Taut by Th70, Th76;
q => (p => q) in IPC-Taut by INTPRO_1:def 14;
then A2: ((p => FALSUM) => (p => q)) '&' (q => (p => q)) in IPC-Taut by A1, INTPRO_1:34;
(((p => FALSUM) => (p => q)) '&' (q => (p => q))) => (((p => FALSUM) 'or' q) => (p => q)) in IPC-Taut by Th70, Th77;
then ((p => FALSUM) 'or' q) => (p => q) in IPC-Taut by A2, INTPRO_1:def 14;
hence |-_IPC ((p => FALSUM) 'or' q) => (p => q) by Th69; :: thesis: verum