Theorem alrimih 1493

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 1479	. 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 1471  ax-gen 1473

This theorem is referenced by:  albidh  1504  alrimi  1546  nfd  1547  19.21h  1581  exlimd2  1619  exlimdh  1620  eximdh  1635  nexd  1637  exbidh  1638  hbex  1660  hbnd  1679  19.12  1689  19.38  1700  ax11i  1738  equsalh  1750  nfald  1784  nfexd  1785  aev  1836  equs5or  1854  sb4or  1857  sbbidh  1869  sb6rf  1877  alrimiv  1898  eupicka  2136  2moex  2142