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