Theorem alrimih 1401

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

Syntax hints:   → wi 4  ∀wal 1285

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

This theorem is referenced by:  albidh  1412  alrimi  1458  nfd  1459  19.21h  1492  exlimd2  1529  exlimdh  1530  eximdh  1545  nexd  1547  exbidh  1548  hbex  1570  hbnd  1588  19.12  1598  19.38  1609  ax11i  1646  equsalh  1658  nfald  1687  nfexd  1688  aev  1737  equs5or  1755  sb4or  1758  sbbidh  1770  sb6rf  1778  alrimiv  1799  eupicka  2025  2moex  2031