let p, q be Element of MC-wff ; :: thesis: |-_IPC ((p => FALSUM) 'or' (q => FALSUM)) => ((p '&' q) => FALSUM)
A1: (((p => FALSUM) => ((p '&' q) => FALSUM)) '&' ((q => FALSUM) => ((p '&' q) => FALSUM))) => (((p => FALSUM) 'or' (q => FALSUM)) => ((p '&' q) => FALSUM)) in IPC-Taut by Th70, Th77;
A2: (p '&' q) => p in IPC-Taut by INTPRO_1:def 14;
((p '&' q) => p) => ((p => FALSUM) => ((p '&' q) => FALSUM)) in IPC-Taut by Th70, Th81;
then A3: (p => FALSUM) => ((p '&' q) => FALSUM) in IPC-Taut by A2, INTPRO_1:def 14;
A4: (p '&' q) => q in IPC-Taut by INTPRO_1:def 14;
((p '&' q) => q) => ((q => FALSUM) => ((p '&' q) => FALSUM)) in IPC-Taut by Th70, Th81;
then (q => FALSUM) => ((p '&' q) => FALSUM) in IPC-Taut by A4, INTPRO_1:def 14;
then ((p => FALSUM) => ((p '&' q) => FALSUM)) '&' ((q => FALSUM) => ((p '&' q) => FALSUM)) in IPC-Taut by A3, INTPRO_1:34;
then ((p => FALSUM) 'or' (q => FALSUM)) => ((p '&' q) => FALSUM) in IPC-Taut by A1, INTPRO_1:def 14;
hence |-_IPC ((p => FALSUM) 'or' (q => FALSUM)) => ((p '&' q) => FALSUM) by Th69; :: thesis: verum