Theorem alrimih 1845

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

Syntax hints:   → wi 4  ∀wal 1559

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

This theorem is referenced by:  nexdh  1886  albidh  1887  alrimiv  1948  ax12i  1987  cbvaliw  2027  nf5dh  2182  nfexhe  2211  alrimi  2249  hbnd  2331  cbv3v  2367  cbv3  2429  eujustALT  2600  axi5r  2727  hbralrimi  3153  ralidmw  4471  bnj1093  35276  bj-abvALT  37393  bj-gabssd  37422  mpobi123f  38662  axc4i-o  39523  equidq  39549  aev-o  39556  ax12f  39565  axc5c4c711  44978  hbimpg  45131  gen11nv  45194