Theorem alrimih 1824

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2208 and 19.21h 2288. 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  2297  cbv3v  2337  cbv3  2402  eujustALT  2572  axi5r  2700  hbralrimi  3131  ralidmw  4488  bnj1093  35016  bj-abvALT  36930  bj-gabssd  36959  mpobi123f  38191  axc4i-o  38921  equidq  38947  aev-o  38954  ax12f  38963  axc5c4c711  44400  hbimpg  44554  gen11nv  44617