let p, q, r be Element of MC-wff ; |-_IPC (p => q) => (((q 'or' r) => FALSUM) => ((p 'or' r) => FALSUM))
p 'or' r in {(p 'or' r),((q 'or' r) => FALSUM),(p => q)}
by ENUMSET1:def 1;
then A1:
{(p 'or' r),((q 'or' r) => FALSUM),(p => q)} |-_IPC p 'or' r
by Th67;
(q 'or' r) => FALSUM in {(p 'or' r),((q 'or' r) => FALSUM),(p => q)}
by ENUMSET1:def 1;
then A2:
{(p 'or' r),((q 'or' r) => FALSUM),(p => q)} |-_IPC (q 'or' r) => FALSUM
by Th67;
p => q in {(p 'or' r),((q 'or' r) => FALSUM),(p => q)}
by ENUMSET1:def 1;
then A3:
{(p 'or' r),((q 'or' r) => FALSUM),(p => q)} |-_IPC p => q
by Th67;
A04:
|-_IPC (p => q) => ((p 'or' r) => (q 'or' r))
by Th69, INTPRO_1:60;
{} MC-wff c= {(p 'or' r),((q 'or' r) => FALSUM),(p => q)}
;
then
{(p 'or' r),((q 'or' r) => FALSUM),(p => q)} |-_IPC (p => q) => ((p 'or' r) => (q 'or' r))
by A04, Th66;
then
{(p 'or' r),((q 'or' r) => FALSUM),(p => q)} |-_IPC (p 'or' r) => (q 'or' r)
by A3, Th27;
then
{(p 'or' r),((q 'or' r) => FALSUM),(p => q)} |-_IPC q 'or' r
by A1, Th27;
then
{(p 'or' r),((q 'or' r) => FALSUM),(p => q)} |-_IPC FALSUM
by A2, Th27;
then
{((q 'or' r) => FALSUM),(p => q)} |-_IPC (p 'or' r) => FALSUM
by Th56;
then
{(p => q)} |-_IPC ((q 'or' r) => FALSUM) => ((p 'or' r) => FALSUM)
by Th55;
hence
|-_IPC (p => q) => (((q 'or' r) => FALSUM) => ((p 'or' r) => FALSUM))
by Th54; verum