Theorem alrimih 1857

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2244 and 19.21h 2321. 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  2250  hbnd  2330  cbv3v  2365  cbv3  2427  eujustALT  2598  axi5r  2725  hbralrimi  3153  ralidmw  4472  bnj1093  35610  bj-abvALT  37819  bj-gabssd  37849  mpobi123f  39094  axc4i-o  39955  equidq  39981  aev-o  39988  ax12f  39997  axc5c4c711  45384  hbimpg  45536  gen11nv  45599