Theorem alrimih 1825

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

Syntax hints:   → wi 4  ∀wal 1539

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

This theorem is referenced by:  nexdh  1866  albidh  1867  alrimiv  1928  ax12i  1967  cbvaliw  2007  nf5dh  2152  nfexhe  2182  alrimi  2220  hbnd  2302  cbv3v  2339  cbv3  2401  eujustALT  2572  axi5r  2700  hbralrimi  3126  ralidmw  4469  bnj1093  35138  bj-abvALT  37110  bj-gabssd  37139  mpobi123f  38365  axc4i-o  39180  equidq  39206  aev-o  39213  ax12f  39222  axc5c4c711  44663  hbimpg  44816  gen11nv  44879