Theorem alrimih 1518

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

Syntax hints:   → wi 4  ∀wal 1396

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

This theorem is referenced by:  albidh  1529  alrimi  1571  nfd  1572  19.21h  1606  exlimd2  1644  exlimdh  1645  eximdh  1660  nexd  1662  exbidh  1663  hbex  1685  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