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  2395  eujustALT  2565  axi5r  2694  hbralrimi  3137  ralidmw  4470  bnj1093  33681  bj-abvALT  35450  bj-gabssd  35479  mpobi123f  36694  axc4i-o  37433  equidq  37459  aev-o  37466  ax12f  37475  axc5c4c711  42803  hbimpg  42958  gen11nv  43021