Theorem alrimih 1830

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2209 and 19.21h 2291. Instance of sylg 1829. (Contributed by NM, 9-Jan-1993.) (Revised by BJ, 31-Mar-2021.)

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 1829	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1802  ax-4 1816

This theorem is referenced by:  nexdh  1872  albidh  1873  alrimiv  1934  ax12i  1974  cbvaliw  2018  nf5dh  2151  alrimi  2215  hbnd  2300  cbv3v  2337  cbv3  2397  eujustALT  2573  axi5r  2702  hbralrimi  3094  ralidmw  4394  bnj1093  32531  bj-abvALT  34736  bj-gabssd  34767  mpobi123f  35963  axc4i-o  36555  equidq  36581  aev-o  36588  ax12f  36597  axc5c4c711  41577  hbimpg  41732  gen11nv  41795