Theorem alrimih 1826

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

Syntax hints:   → wi 4  ∀wal 1539

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

This theorem is referenced by:  nexdh  1868  albidh  1869  alrimiv  1930  ax12i  1970  cbvaliw  2009  nf5dh  2143  alrimi  2206  hbnd  2292  cbv3v  2331  cbv3  2396  eujustALT  2566  axi5r  2695  hbralrimi  3144  ralidmw  4507  bnj1093  34060  bj-abvALT  35873  bj-gabssd  35902  mpobi123f  37116  axc4i-o  37854  equidq  37880  aev-o  37887  ax12f  37896  axc5c4c711  43242  hbimpg  43397  gen11nv  43460