Theorem alrimih 1857

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2246 and 19.21h 2324. 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  2185  nfexhe  2214  alrimi  2252  hbnd  2333  cbv3v  2369  cbv3  2431  eujustALT  2602  axi5r  2729  hbralrimi  3157  ralidmw  4479  bnj1093  35437  bj-abvALT  37603  bj-gabssd  37633  mpobi123f  38873  axc4i-o  39734  equidq  39760  aev-o  39767  ax12f  39776  axc5c4c711  45188  hbimpg  45340  gen11nv  45403