Theorem alrimih 1518

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)

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	. . 3 ⊢ (𝜑 → 𝜓)
3	2	alimi 1504	. 2 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
4	1, 3	syl 14	1 ⊢ (𝜑 → ∀𝑥𝜓)

Syntax hints:   → wi 4  ∀wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1496  ax-gen 1498

This theorem is referenced by:  albidh  1529  alrimi  1571  nfd  1572  19.21h  1606  exlimd2  1644  exlimdh  1645  eximdh  1660  nexd  1662  exbidh  1663  hbex  1685  hbnd  1703  19.12  1713  19.38  1724  ax11i  1762  equsalh  1774  nfald  1809  nfexd  1810  aev  1861  equs5or  1879  sb4or  1882  sbbidh  1894  sb6rf  1902  alrimiv  1923  eupicka  2161  2moex  2167