Theorem alrimih 1824

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

Syntax hints:   → wi 4  ∀wal 1535

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

This theorem is referenced by:  nexdh  1866  albidh  1867  alrimiv  1928  ax12i  1969  cbvaliw  2013  nf5dh  2151  alrimi  2213  sbbibOLD  2289  hbnd  2304  cbv3v  2355  cbv3  2415  cbvalvOLD  2420  eujustALT  2657  axi5r  2785  hbralrimi  3180  bnj1093  32252  bj-abv  34226  bj-ab0  34227  mpobi123f  35455  axc4i-o  36049  equidq  36075  aev-o  36082  ax12f  36091  axc5c4c711  40753  hbimpg  40908  gen11nv  40971