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\forall y\neg \forall x\forall y\phi \to \forall x\phi \right)\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		ax-c5	$$⊢\forall y\phi \to \phi$$
2		ax10fromc7	$$⊢\neg \forall y\phi \to \forall y\neg \forall y\phi$$
3		ax-c7	$$⊢\neg \forall x\neg \forall x\forall y\phi \to \forall y\phi$$
4	3	con1i	$$⊢\neg \forall y\phi \to \forall x\neg \forall x\forall y\phi$$
5	4	alimi	$$⊢\forall y\neg \forall y\phi \to \forall y\forall x\neg \forall x\forall y\phi$$
6		ax-11	$$⊢\forall y\forall x\neg \forall x\forall y\phi \to \forall x\forall y\neg \forall x\forall y\phi$$
7	2 5 6	3syl	$$⊢\neg \forall y\phi \to \forall x\forall y\neg \forall x\forall y\phi$$
8	1 7	nsyl4	$$⊢\neg \forall x\forall y\neg \forall x\forall y\phi \to \phi$$
9		ax-c5	$$⊢\forall x\phi \to \phi$$
10	8 9	ja	$$⊢\left(\forall x\forall y\neg \forall x\forall y\phi \to \forall x\phi \right)\to \phi$$