Theorem alrimih 1565

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
alrimih	⊢ (φ → ∀xψ)

Proof of Theorem alrimih

Step	Hyp	Ref	Expression
1		alrimih.1	. 2 ⊢ (φ → ∀xφ)
2		alrimih.2	. . 3 ⊢ (φ → ψ)
3	2	alimi 1559	. 2 ⊢ (∀xφ → ∀xψ)
4	1, 3	syl 15	1 ⊢ (φ → ∀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-5 1557

This theorem is referenced by:  eximdh  1588  nexdh  1589  albidh  1590  exbidh  1591  alrimiv  1631  ax11i  1647  cbvaliw  1673  alrimi  1765  hbnOLD  1777  hbimdOLD  1816  hbimOLD  1818  19.23hOLD  1820  spimehOLD  1821  equsalhwOLD  1839  19.21hOLD  1840  19.12OLD  1848  cbv3hvOLD  1851  hbnd  1883  dvelimv  1939  a16g  1945  aev  1991  a5i-o  2150  equidq  2175  aev-o  2182  ax11f  2192  eujustALT  2207