Theorem alrimih 1822

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2208 and 19.21h 2291. Instance of sylg 1821. (Contributed by NM, 9-Jan-1993.)

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 1821	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1535

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

This theorem is referenced by:  nexdh  1864  albidh  1865  alrimiv  1926  ax12i  1966  cbvaliw  2005  nf5dh  2147  alrimi  2214  hbnd  2300  cbv3v  2341  cbv3  2405  eujustALT  2575  axi5r  2703  hbralrimi  3150  ralidmw  4531  bnj1093  34956  bj-abvALT  36873  bj-gabssd  36902  mpobi123f  38122  axc4i-o  38854  equidq  38880  aev-o  38887  ax12f  38896  axc5c4c711  44370  hbimpg  44525  gen11nv  44588