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