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	⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sp	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )
2		hbn1	⊢ ( ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 𝜑 )
3	1 2	nsyl4	⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → 𝜑 )