Theorem alrimih 1826

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

Syntax hints:   → wi 4  ∀wal 1540

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  1867  albidh  1868  alrimiv  1929  ax12i  1968  cbvaliw  2008  nf5dh  2153  nfexhe  2183  alrimi  2221  hbnd  2303  cbv3v  2340  cbv3  2402  eujustALT  2573  axi5r  2701  hbralrimi  3128  ralidmw  4457  bnj1093  35141  bj-abvALT  37233  bj-gabssd  37262  mpobi123f  38500  axc4i-o  39361  equidq  39387  aev-o  39394  ax12f  39403  axc5c4c711  44849  hbimpg  45002  gen11nv  45065