Theorem alrimih 1827

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

Syntax hints:   → wi 4  ∀wal 1537

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

This theorem is referenced by:  nexdh  1869  albidh  1870  alrimiv  1931  ax12i  1971  cbvaliw  2010  nf5dh  2145  alrimi  2209  hbnd  2296  cbv3v  2334  cbv3  2397  eujustALT  2572  axi5r  2701  hbralrimi  3105  ralidmw  4435  bnj1093  32860  bj-abvALT  35019  bj-gabssd  35051  mpobi123f  36247  axc4i-o  36839  equidq  36865  aev-o  36872  ax12f  36881  axc5c4c711  41908  hbimpg  42063  gen11nv  42126