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

Proof

Step	Hyp	Ref	Expression
1		ax-c4	⊢ ( ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 𝜑 → 𝜓 ) ) → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( ∀ 𝑥 𝜑 → 𝜓 ) ) )
2		ax-c5	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )
3		ax-c5	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) )
4	2 3	syl5	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 𝜑 → 𝜓 ) )
5	1 4	mpg	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( ∀ 𝑥 𝜑 → 𝜓 ) )
6		ax-c4	⊢ ( ∀ 𝑥 ( ∀ 𝑥 𝜑 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) )
7	5 6	syl	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) )