Theorem axc4

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

	Ref	Expression
Assertion	axc4	$$⊢\forall x\left(\forall x\phi \to \psi \right)\to \left(\forall x\phi \to \forall x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sp	$$⊢\forall x\neg \forall x\phi \to \neg \forall x\phi$$
2	1	con2i	$$⊢\forall x\phi \to \neg \forall x\neg \forall x\phi$$
3		hbn1	$$⊢\neg \forall x\neg \forall x\phi \to \forall x\neg \forall x\neg \forall x\phi$$
4		hbn1	$$⊢\neg \forall x\phi \to \forall x\neg \forall x\phi$$
5	4	con1i	$$⊢\neg \forall x\neg \forall x\phi \to \forall x\phi$$
6	5	alimi	$$⊢\forall x\neg \forall x\neg \forall x\phi \to \forall x\forall x\phi$$
7	2 3 6	3syl	$$⊢\forall x\phi \to \forall x\forall x\phi$$
8		alim	$$⊢\forall x\left(\forall x\phi \to \psi \right)\to \left(\forall x\forall x\phi \to \forall x\psi \right)$$
9	7 8	syl5	$$⊢\forall x\left(\forall x\phi \to \psi \right)\to \left(\forall x\phi \to \forall x\psi \right)$$