Theorem alrimih 1492

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

Syntax hints:   → wi 4  ∀wal 1371

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

This theorem is referenced by:  albidh  1503  alrimi  1545  nfd  1546  19.21h  1580  exlimd2  1618  exlimdh  1619  eximdh  1634  nexd  1636  exbidh  1637  hbex  1659  hbnd  1678  19.12  1688  19.38  1699  ax11i  1737  equsalh  1749  nfald  1783  nfexd  1784  aev  1835  equs5or  1853  sb4or  1856  sbbidh  1868  sb6rf  1876  alrimiv  1897  eupicka  2134  2moex  2140