Theorem alrimih 1854

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1825  ax-4 1839

This theorem is used by:  nexdh  1895  albidh  1896  alrimiv  1957  ax12i  1996  cbvaliw  2036  nf5dh  2182  nfexhe  2211  alrimi  2249  hbnd  2331  cbv3v  2367  cbv3  2429  eujustALT  2600  axi5r  2727  hbralrimi  3155  ralidmw  4477  bnj1093  35377  bj-abvALT  37570  bj-gabssd  37600  mpobi123f  38839  axc4i-o  39700  equidq  39726  aev-o  39733  ax12f  39742  axc5c4c711  45139  hbimpg  45291  gen11nv  45354