Theorem ax4fromc4

Description: Rederivation of Axiom ax-4 from ax-c4 , ax-c5 , ax-gen and minimal implicational calculus { ax-mp , ax-1 , ax-2 }. See axc4 for the derivation of ax-c4 from ax-4 . (Contributed by NM, 23-May-2008) (Proof modification is discouraged.) Use ax-4 instead. (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax-c4	$$⊢\forall x\left(\forall x\left(\phi \to \psi \right)\to \left(\forall x\phi \to \psi \right)\right)\to \left(\forall x\left(\phi \to \psi \right)\to \forall x\left(\forall x\phi \to \psi \right)\right)$$
2		ax-c5	$$⊢\forall x\phi \to \phi$$
3		ax-c5	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\phi \to \psi \right)$$
4	2 3	syl5	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\forall x\phi \to \psi \right)$$
5	1 4	mpg	$$⊢\forall x\left(\phi \to \psi \right)\to \forall x\left(\forall x\phi \to \psi \right)$$
6		ax-c4	$$⊢\forall x\left(\forall x\phi \to \psi \right)\to \left(\forall x\phi \to \forall x\psi \right)$$
7	5 6	syl	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\forall x\phi \to \forall x\psi \right)$$