Theorem ax5 2146

Description: Rederivation of axiom ax-5 1557 from ax-5o 2136 and other older axioms. See ax5o 1749 for the derivation of ax-5o 2136 from ax-5 1557. (Contributed by NM, 23-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
ax5	⊢ (∀x(φ → ψ) → (∀xφ → ∀xψ))

Proof of Theorem ax5

Step	Hyp	Ref	Expression
1		ax-5o 2136	. . 3 ⊢ (∀x(∀x(φ → ψ) → (∀xφ → ψ)) → (∀x(φ → ψ) → ∀x(∀xφ → ψ)))
2		ax-4 2135	. . . 4 ⊢ (∀xφ → φ)
3		ax-4 2135	. . . 4 ⊢ (∀x(φ → ψ) → (φ → ψ))
4	2, 3	syl5 28	. . 3 ⊢ (∀x(φ → ψ) → (∀xφ → ψ))
5	1, 4	mpg 1548	. 2 ⊢ (∀x(φ → ψ) → ∀x(∀xφ → ψ))
6		ax-5o 2136	. 2 ⊢ (∀x(∀xφ → ψ) → (∀xφ → ∀xψ))
7	5, 6	syl 15	1 ⊢ (∀x(φ → ψ) → (∀xφ → ∀xψ))

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1546  ax-4 2135  ax-5o 2136

This theorem is referenced by: (None)