Theorem alrimih 1857

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2243 and 19.21h 2320. Instance of sylg 1856. (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 1856	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 1828  ax-4 1842

This theorem is used by:  nexdh  1898  albidh  1899  alrimiv  1960  ax12i  1999  cbvaliw  2039  nf5dh  2184  nfexhe  2211  alrimi  2249  hbnd  2329  cbv3v  2364  cbv3  2426  eujustALT  2597  axi5r  2724  hbralrimi  3152  ralidmw  4472  bnj1093  35492  bj-abvALT  37653  bj-gabssd  37683  mpobi123f  38913  axc4i-o  39774  equidq  39800  aev-o  39807  ax12f  39816  axc5c4c711  45228  hbimpg  45380  gen11nv  45443