Theorem alrimih 1824

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

Syntax hints:   → wi 4  ∀wal 1538

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

This theorem is referenced by:  nexdh  1865  albidh  1866  alrimiv  1927  ax12i  1966  cbvaliw  2006  nf5dh  2148  alrimi  2214  hbnd  2296  cbv3v  2333  cbv3  2395  eujustALT  2565  axi5r  2693  hbralrimi  3119  ralidmw  4459  bnj1093  34947  bj-abvALT  36881  bj-gabssd  36910  mpobi123f  38142  axc4i-o  38877  equidq  38903  aev-o  38910  ax12f  38919  axc5c4c711  44374  hbimpg  44528  gen11nv  44591