Theorem alrimih 1824

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

Syntax hints:   → wi 4  ∀wal 1538

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

This theorem is referenced by:  nexdh  1865  albidh  1866  alrimiv  1927  ax12i  1966  cbvaliw  2006  nf5dh  2148  alrimi  2214  hbnd  2296  cbv3v  2333  cbv3  2395  eujustALT  2565  axi5r  2693  hbralrimi  3123  ralidmw  4471  bnj1093  34970  bj-abvALT  36895  bj-gabssd  36924  mpobi123f  38156  axc4i-o  38891  equidq  38917  aev-o  38924  ax12f  38933  axc5c4c711  44390  hbimpg  44544  gen11nv  44607