Metamath Proof Explorer

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 ⊢ ∀ x φ → ψ → ∀ x φ → ∀ x ψ

Proof

Step Hyp Ref Expression
1 ax-c4 ⊢ ∀ x ∀ x φ → ψ → ∀ x φ → ψ → ∀ x φ → ψ → ∀ x ∀ x φ → ψ
2 ax-c5 ⊢ ∀ x φ → φ
3 ax-c5 ⊢ ∀ x φ → ψ → φ → ψ
4 2 3 syl5 ⊢ ∀ x φ → ψ → ∀ x φ → ψ
5 1 4 mpg ⊢ ∀ x φ → ψ → ∀ x ∀ x φ → ψ
6 ax-c4 ⊢ ∀ x ∀ x φ → ψ → ∀ x φ → ∀ x ψ
7 5 6 syl ⊢ ∀ x φ → ψ → ∀ x φ → ∀ x ψ