Theorem alrimih 1831

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

Syntax hints:   → wi 4  ∀wal 1545

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

This theorem is referenced by:  nexdh  1872  albidh  1873  alrimiv  1934  ax12i  1973  cbvaliw  2013  nf5dh  2158  nfexhe  2187  alrimi  2225  hbnd  2307  cbv3v  2343  cbv3  2405  eujustALT  2576  axi5r  2703  hbralrimi  3129  ralidmw  4445  bnj1093  35171  bj-abvALT  37269  bj-gabssd  37298  mpobi123f  38538  axc4i-o  39399  equidq  39425  aev-o  39432  ax12f  39441  axc5c4c711  44854  hbimpg  45007  gen11nv  45070