Theorem axc7

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.)

Conclusion
\( \vdash \neg \forall x \, \neg \forall x \, \varphi \rightarrow \varphi \)
Proof
l0
sp
\( \vdash \forall x \, \varphi \rightarrow \varphi \)
hbn1
\( \vdash \neg \forall x \, \varphi \rightarrow \forall x \, \neg \forall x \, \varphi \)
nsyl4 l0 _