Theorem alrimih 1826

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2200 and 19.21h 2284. 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 1537

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  1868  albidh  1869  alrimiv  1930  ax12i  1970  cbvaliw  2009  nf5dh  2143  alrimi  2206  hbnd  2293  cbv3v  2332  cbv3  2397  eujustALT  2572  axi5r  2701  hbralrimi  3101  ralidmw  4438  bnj1093  32960  bj-abvALT  35092  bj-gabssd  35124  mpobi123f  36320  axc4i-o  36912  equidq  36938  aev-o  36945  ax12f  36954  axc5c4c711  42019  hbimpg  42174  gen11nv  42237