Metamath Proof Explorer

Theorem axc5c711

Description: Proof of a single axiom that can replace ax-c5 , ax-c7 , and ax-11 in a subsystem that includes these axioms plus ax-c4 and ax-gen (and propositional calculus). See axc5c711toc5 , axc5c711toc7 , and axc5c711to11 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 . (Contributed by NM, 18-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axc5c711 ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {\phi }$

Proof

Step Hyp Ref Expression
1 ax-c5 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }$
2 ax10fromc7 ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 ax-c7 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 3 con1i ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
5 4 alimi ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
6 ax-11 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
7 2 5 6 3syl ${⊢}¬\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
8 1 7 nsyl4 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }$
9 ax-c5 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\phi }$
10 8 9 ja ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {\phi }$