Theorem a5i 687

Description: Inference from ax-5 674.

Hypothesis

Ref	Expression
a5i.1	⊢ (∀xφ → ψ)

Assertion

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

Proof of Theorem a5i

Step	Hyp	Ref	Expression
1		ax-5 674	. 2 ⊢ (∀x(∀xφ → ψ) → (∀xφ → ∀xψ))
2		a5i.1	. 2 ⊢ (∀xφ → ψ)
3	1, 2	mpg 684	1 ⊢ (∀xφ → ∀xψ)

Syntax hints:   → wi 2  ∀wal 672

This theorem is referenced by:  19.20 690  19.20i 691  hba1 698  eq5 824  eqs1 828  eqsal 833  hbsb2 873  hbs1f 874  exists2 1073  axunndlem1 3741  axregnd 3750  axacndlem3 3755  axacndlem5 3757  axacnd 3758

This theorem was proved from axioms:  ax-mp 6  ax-5 674  ax-gen 677

metamath.org