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