Theorem axc7

Description: Show that the original axiom ax-c7 can be derived from ax-10 ( hbn1 ), sp and propositional calculus. See ax10fromc7 for the rederivation of ax-10 from ax-c7 .

Normally, axc7 should be used rather than ax-c7 , except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008)

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

Proof

Step	Hyp	Ref	Expression
1		sp	$$⊢\forall x\phi \to \phi$$
2		hbn1	$$⊢\neg \forall x\phi \to \forall x\neg \forall x\phi$$
3	1 2	nsyl4	$$⊢\neg \forall x\neg \forall x\phi \to \phi$$