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