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