Theorem alrimih 1480

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

Syntax hints:   → wi 4  ∀wal 1362

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

This theorem is referenced by:  albidh  1491  alrimi  1533  nfd  1534  19.21h  1568  exlimd2  1606  exlimdh  1607  eximdh  1622  nexd  1624  exbidh  1625  hbex  1647  hbnd  1666  19.12  1676  19.38  1687  ax11i  1725  equsalh  1737  nfald  1771  nfexd  1772  aev  1823  equs5or  1841  sb4or  1844  sbbidh  1856  sb6rf  1864  alrimiv  1885  eupicka  2118  2moex  2124