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  4471  bnj1093  35160  bj-abvALT  37159  bj-gabssd  37188  mpobi123f  38417  axc4i-o  39278  equidq  39304  aev-o  39311  ax12f  39320  axc5c4c711  44761  hbimpg  44914  gen11nv  44977