Theorem alrimih 1818

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2195 and 19.21h 2276. Instance of sylg 1817. (Contributed by NM, 9-Jan-1993.) (Revised by BJ, 31-Mar-2021.)

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 1817	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1531

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

This theorem is referenced by:  nexdh  1860  albidh  1861  alrimiv  1922  ax12i  1962  cbvaliw  2001  nf5dh  2135  alrimi  2201  hbnd  2285  cbv3v  2326  cbv3  2391  eujustALT  2561  axi5r  2691  hbralrimi  3141  ralidmw  4511  bnj1093  34644  bj-abvALT  36418  bj-gabssd  36447  mpobi123f  37668  axc4i-o  38402  equidq  38428  aev-o  38435  ax12f  38444  axc5c4c711  43869  hbimpg  44024  gen11nv  44087