Theorem axc4
Show that the original axiom [ax-c4] can be derived from [ax-4]
( alim ), [ax-10] ( hbn1 ), sp and propositional calculus. See
[ax4fromc4] for the rederivation of [ax-4] from [ax-c4].
Part of the proof is based on the proof of Lemma 22 of [Monk2] p. 114.
(Contributed by NM, 21-May-2008.) (Proof modification is discouraged.)
Conclusion
\( \vdash \forall x \, (\forall x \, \varphi \rightarrow \psi) \rightarrow \forall x \, \varphi \rightarrow \forall x \, \psi \)
Proof
sp
l1
con2i _
\( \vdash \forall x \, \varphi \rightarrow \neg \forall x \, \neg \forall x \, \varphi \)
l2
hbn1
\( \vdash \neg \forall x \, \neg \forall x \, \varphi \rightarrow \forall x \, \neg \forall x \, \neg \forall x \, \varphi \)
hbn1
con1i _
alimi _
\( \vdash \forall x \, \neg \forall x \, \neg \forall x \, \varphi \rightarrow \forall x \, \forall x \, \varphi \)
l6
3syl l1 l2 _
\( \vdash \forall x \, \varphi \rightarrow \forall x \, \forall x \, \varphi \)
alim
\( \vdash \forall x \, (\forall x \, \varphi \rightarrow \psi) \rightarrow \forall x \, \forall x \, \varphi \rightarrow \forall x \, \psi \)
syl5 l6 _