Theorem ax10fromc7

Description: Rederivation of Axiom ax-10 from ax-c7 , ax-c4 , ax-c5 , ax-gen and propositional calculus. See axc7 for the derivation of ax-c7 from ax-10 . (Contributed by NM, 23-May-2008) (Proof modification is discouraged.) Use ax-10 instead. (New usage is discouraged.)

	Ref	Expression
Assertion	ax10fromc7	$$⊢\neg \forall x\phi \to \forall x\neg \forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		ax-c4	$$⊢\forall x\left(\forall x\neg \forall x\forall x\phi \to \neg \forall x\phi \right)\to \left(\forall x\neg \forall x\forall x\phi \to \forall x\neg \forall x\phi \right)$$
2		ax-c5	$$⊢\forall x\neg \forall x\forall x\phi \to \neg \forall x\forall x\phi$$
3		ax-c4	$$⊢\forall x\left(\forall x\phi \to \forall x\phi \right)\to \left(\forall x\phi \to \forall x\forall x\phi \right)$$
4		id	$$⊢\forall x\phi \to \forall x\phi$$
5	3 4	mpg	$$⊢\forall x\phi \to \forall x\forall x\phi$$
6	2 5	nsyl	$$⊢\forall x\neg \forall x\forall x\phi \to \neg \forall x\phi$$
7	1 6	mpg	$$⊢\forall x\neg \forall x\forall x\phi \to \forall x\neg \forall x\phi$$
8		ax-c7	$$⊢\neg \forall x\neg \forall x\forall x\phi \to \forall x\phi$$
9	7 8	nsyl4	$$⊢\neg \forall x\phi \to \forall x\neg \forall x\phi$$