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