Theorem alrimih 1827

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

Syntax hints:   → wi 4  ∀wal 1540

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

This theorem is referenced by:  nexdh  1869  albidh  1870  alrimiv  1931  ax12i  1971  cbvaliw  2010  nf5dh  2144  alrimi  2207  hbnd  2293  cbv3v  2332  cbv3  2397  eujustALT  2567  axi5r  2696  hbralrimi  3145  ralidmw  4508  bnj1093  33991  bj-abvALT  35787  bj-gabssd  35816  mpobi123f  37030  axc4i-o  37768  equidq  37794  aev-o  37801  ax12f  37810  axc5c4c711  43160  hbimpg  43315  gen11nv  43378