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