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  3123  ralidmw  4467  bnj1093  34963  bj-abvALT  36888  bj-gabssd  36917  mpobi123f  38149  axc4i-o  38884  equidq  38910  aev-o  38917  ax12f  38926  axc5c4c711  44383  hbimpg  44537  gen11nv  44600