Theorem alrimih 1851

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2249 and 19.21h 2328. Instance of sylg 1850. (Contributed by NM, 9-Jan-1993.)

Hypotheses

Ref	Expression
alrimih.1	⊢ (𝜑 → ∀𝑥𝜑)
alrimih.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
alrimih	⊢ (𝜑 → ∀𝑥𝜓)

Proof of Theorem alrimih

Step	Hyp	Ref	Expression
1		alrimih.1	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		alrimih.2	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	sylg 1850	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1822  ax-4 1836

This theorem is referenced by:  nexdh  1892  albidh  1893  alrimiv  1954  ax12i  1993  cbvaliw  2033  nf5dh  2188  nfexhe  2217  alrimi  2255  hbnd  2337  cbv3v  2373  cbv3  2435  eujustALT  2606  axi5r  2733  hbralrimi  3161  ralidmw  4482  bnj1093  35313  bj-abvALT  37465  bj-gabssd  37494  mpobi123f  38735  axc4i-o  39596  equidq  39622  aev-o  39629  ax12f  39638  axc5c4c711  45037  hbimpg  45189  gen11nv  45252