Theorem alrimih 1823

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

Syntax hints:   → wi 4  ∀wal 1537

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

This theorem is referenced by:  nexdh  1864  albidh  1865  alrimiv  1926  ax12i  1965  cbvaliw  2004  nf5dh  2146  alrimi  2212  hbnd  2295  cbv3v  2336  cbv3  2401  eujustALT  2571  axi5r  2699  hbralrimi  3143  ralidmw  4507  bnj1093  34995  bj-abvALT  36909  bj-gabssd  36938  mpobi123f  38170  axc4i-o  38900  equidq  38926  aev-o  38933  ax12f  38942  axc5c4c711  44425  hbimpg  44579  gen11nv  44642