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