Theorem alrimih 1515

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

Syntax hints:   → wi 4  ∀wal 1393

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

This theorem is referenced by:  albidh  1526  alrimi  1568  nfd  1569  19.21h  1603  exlimd2  1641  exlimdh  1642  eximdh  1657  nexd  1659  exbidh  1660  hbex  1682  hbnd  1701  19.12  1711  19.38  1722  ax11i  1760  equsalh  1772  nfald  1806  nfexd  1807  aev  1858  equs5or  1876  sb4or  1879  sbbidh  1891  sb6rf  1899  alrimiv  1920  eupicka  2158  2moex  2164