Theorem alrimih 1820

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

Syntax hints:   → wi 4  ∀wal 1531

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

This theorem is referenced by:  nexdh  1862  albidh  1863  alrimiv  1924  ax12i  1965  cbvaliw  2009  nf5dh  2147  alrimi  2209  sbbibOLD  2285  hbnd  2300  cbv3v  2351  cbv3  2411  cbvalvOLD  2416  eujustALT  2653  axi5r  2783  hbralrimi  3180  bnj1093  32247  bj-abv  34218  bj-ab0  34219  mpobi123f  35434  axc4i-o  36028  equidq  36054  aev-o  36061  ax12f  36070  axc5c4c711  40726  hbimpg  40881  gen11nv  40944