Theorem alrimih 1825

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

Syntax hints:   → wi 4  ∀wal 1536

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  1866  albidh  1867  alrimiv  1928  ax12i  1969  cbvaliw  2013  nf5dh  2148  alrimi  2211  sbbibOLD  2285  hbnd  2300  cbv3v  2344  cbv3  2404  cbvalvOLD  2409  eujustALT  2632  axi5r  2762  hbralrimi  3147  bnj1093  32362  bj-abv  34347  bj-ab0  34348  mpobi123f  35600  axc4i-o  36194  equidq  36220  aev-o  36227  ax12f  36236  axc5c4c711  41105  hbimpg  41260  gen11nv  41323