let p be Element of MC-wff ; :: thesis: |-_IPC (p => FALSUM) 'equiv' (((p => FALSUM) => FALSUM) => FALSUM)
A1: |-_IPC (p => FALSUM) => (((p => FALSUM) => FALSUM) => FALSUM) by Th102;
|-_IPC (((p => FALSUM) => FALSUM) => FALSUM) => (p => FALSUM) by Th103;
hence |-_IPC (p => FALSUM) 'equiv' (((p => FALSUM) => FALSUM) => FALSUM) by A1, Th84; :: thesis: verum