Theorem alrimih 1825

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2210 and 19.21h 2289. Instance of sylg 1824. (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 1824	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1539

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

This theorem is referenced by:  nexdh  1866  albidh  1867  alrimiv  1928  ax12i  1967  cbvaliw  2007  nf5dh  2150  alrimi  2216  hbnd  2298  cbv3v  2335  cbv3  2397  eujustALT  2567  axi5r  2695  hbralrimi  3122  ralidmw  4455  bnj1093  34992  bj-abvALT  36951  bj-gabssd  36980  mpobi123f  38212  axc4i-o  39007  equidq  39033  aev-o  39040  ax12f  39049  axc5c4c711  44504  hbimpg  44657  gen11nv  44720