let p, q be Element of MC-wff ; |-_IPC (((p '&' q) => FALSUM) => FALSUM) => (((p => FALSUM) => FALSUM) '&' ((q => FALSUM) => FALSUM))
A1:
|-_IPC (p '&' q) => p
by Th30;
A2:
|-_IPC (p '&' q) => q
by Th31;
A3:
|-_IPC ((p '&' q) => p) => ((p => FALSUM) => ((p '&' q) => FALSUM))
by Th81;
A4:
|-_IPC (p => FALSUM) => ((p '&' q) => FALSUM)
by A1, A3, Th37;
|-_IPC ((p => FALSUM) => ((p '&' q) => FALSUM)) => ((((p '&' q) => FALSUM) => FALSUM) => ((p => FALSUM) => FALSUM))
by Th81;
then A6:
|-_IPC (((p '&' q) => FALSUM) => FALSUM) => ((p => FALSUM) => FALSUM)
by A4, Th37;
|-_IPC ((p '&' q) => q) => ((q => FALSUM) => ((p '&' q) => FALSUM))
by Th81;
then A8:
|-_IPC (q => FALSUM) => ((p '&' q) => FALSUM)
by A2, Th37;
|-_IPC ((q => FALSUM) => ((p '&' q) => FALSUM)) => ((((p '&' q) => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))
by Th81;
then A10:
|-_IPC (((p '&' q) => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM)
by A8, Th37;
|-_IPC ((((p '&' q) => FALSUM) => FALSUM) => ((p => FALSUM) => FALSUM)) => (((((p '&' q) => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM)) => ((((p '&' q) => FALSUM) => FALSUM) => (((p => FALSUM) => FALSUM) '&' ((q => FALSUM) => FALSUM))))
by Th69, INTPRO_1:38;
then
|-_IPC ((((p '&' q) => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM)) => ((((p '&' q) => FALSUM) => FALSUM) => (((p => FALSUM) => FALSUM) '&' ((q => FALSUM) => FALSUM)))
by A6, Th37;
hence
|-_IPC (((p '&' q) => FALSUM) => FALSUM) => (((p => FALSUM) => FALSUM) '&' ((q => FALSUM) => FALSUM))
by A10, Th37; verum