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