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