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