Theorem a5i 986

Description: Inference from ax-5o 972.

Hypothesis

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

Assertion

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

Proof of Theorem a5i

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

Syntax hints:   → wi 3  ∀wal 951

This theorem is referenced by:  19.20i 989  hba1 1000  hbae 1141  equs4 1146  equsal 1147  hbs1f 1185  hbsb2a 1200  hbsb2e 1201  aev 1204  hbsb2 1222  ax11indalem 1361  ax11inda2ALT 1362  a12studyALT 1372  exists2 1451  reu3 1921  sbcralt 1980  sbcralgf 1982  axunndlem1 4919  axregnd 4928  axacndlem3 4933  axacndlem5 4935  axacnd 4936

This theorem was proved from axioms:  ax-mp 7  ax-gen 960  ax-5o 972

Copyright terms: Public domain