Theorem alrimih 1824

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

Syntax hints:   → wi 4  ∀wal 1538

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

This theorem is referenced by:  nexdh  1865  albidh  1866  alrimiv  1927  ax12i  1966  cbvaliw  2006  nf5dh  2148  alrimi  2214  hbnd  2296  cbv3v  2333  cbv3  2395  eujustALT  2565  axi5r  2693  hbralrimi  3119  ralidmw  4459  bnj1093  34953  bj-abvALT  36891  bj-gabssd  36920  mpobi123f  38152  axc4i-o  38887  equidq  38913  aev-o  38920  ax12f  38929  axc5c4c711  44384  hbimpg  44538  gen11nv  44601