let p, q be Element of MC-wff ; :: thesis: |-_IPC (q => (p => FALSUM)) => ((p '&' q) => FALSUM)
set U = q => (p => FALSUM);
set X = {(p '&' q),(q => (p => FALSUM))};
A0: ( p '&' q in {(p '&' q),(q => (p => FALSUM))} & q => (p => FALSUM) in {(p '&' q),(q => (p => FALSUM))} ) by TARSKI:def 2;
then A1: {(p '&' q),(q => (p => FALSUM))} |-_IPC q => (p => FALSUM) by Th67;
A2: {(p '&' q),(q => (p => FALSUM))} |-_IPC p '&' q by A0, Th67;
{(p '&' q),(q => (p => FALSUM))} |-_IPC (p '&' q) => p by Th20;
then A4: {(p '&' q),(q => (p => FALSUM))} |-_IPC p by A2, Th27;
{(p '&' q),(q => (p => FALSUM))} |-_IPC (p '&' q) => q by Th21;
then {(p '&' q),(q => (p => FALSUM))} |-_IPC q by A2, Th27;
then {(p '&' q),(q => (p => FALSUM))} |-_IPC p => FALSUM by A1, Th27;
then {(p '&' q),(q => (p => FALSUM))} |-_IPC FALSUM by A4, Th27;
then {(q => (p => FALSUM))} |-_IPC (p '&' q) => FALSUM by Th55;
hence |-_IPC (q => (p => FALSUM)) => ((p '&' q) => FALSUM) by Th54; :: thesis: verum