Theorem alrimih 1428

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

Syntax hints:   → wi 4  ∀wal 1312

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

This theorem is referenced by:  albidh  1439  alrimi  1485  nfd  1486  19.21h  1519  exlimd2  1557  exlimdh  1558  eximdh  1573  nexd  1575  exbidh  1576  hbex  1598  hbnd  1616  19.12  1626  19.38  1637  ax11i  1675  equsalh  1687  nfald  1716  nfexd  1717  aev  1766  equs5or  1784  sb4or  1787  sbbidh  1799  sb6rf  1807  alrimiv  1828  eupicka  2055  2moex  2061