Theorem alrimih 1517

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

Syntax hints:   → wi 4  ∀wal 1395

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

This theorem is referenced by:  albidh  1528  alrimi  1570  nfd  1571  19.21h  1605  exlimd2  1643  exlimdh  1644  eximdh  1659  nexd  1661  exbidh  1662  hbex  1684  hbnd  1703  19.12  1713  19.38  1724  ax11i  1762  equsalh  1774  nfald  1808  nfexd  1809  aev  1860  equs5or  1878  sb4or  1881  sbbidh  1893  sb6rf  1901  alrimiv  1922  eupicka  2160  2moex  2166