let p, q, r be Element of MC-wff ; :: thesis: |-_IPC (p => q) => (((q '&' r) => FALSUM) => ((p '&' r) => FALSUM))
p '&' r in {(p '&' r),((q '&' r) => FALSUM),(p => q)} by ENUMSET1:def 1;
then A1: {(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC p '&' r by Th67;
(q '&' r) => FALSUM in {(p '&' r),((q '&' r) => FALSUM),(p => q)} by ENUMSET1:def 1;
then A2: {(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC (q '&' r) => FALSUM by Th67;
p => q in {(p '&' r),((q '&' r) => FALSUM),(p => q)} by ENUMSET1:def 1;
then A3: {(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC p => q by Th67;
{(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC (p '&' r) => r by Th21;
then A5: {(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC r by A1, Th27;
{(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC (p '&' r) => p by Th20;
then {(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC p by A1, Th27;
then A6: {(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC q by A3, Th27;
{(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC q => (r => (q '&' r)) by Th22;
then {(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC r => (q '&' r) by A6, Th27;
then {(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC q '&' r by A5, Th27;
then {(p '&' r),((q '&' r) => FALSUM),(p => q)} |-_IPC FALSUM by A2, Th27;
then {((q '&' r) => FALSUM),(p => q)} |-_IPC (p '&' r) => FALSUM by Th56;
then {(p => q)} |-_IPC ((q '&' r) => FALSUM) => ((p '&' r) => FALSUM) by Th55;
hence |-_IPC (p => q) => (((q '&' r) => FALSUM) => ((p '&' r) => FALSUM)) by Th54; :: thesis: verum