Theorem alrimih 1446

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	|- ( ph -> A. x ph )
alrimih.2	|- ( ph -> ps )

Assertion

Ref	Expression
alrimih	|- ( ph -> A. x ps )

Proof of Theorem alrimih

Step	Hyp	Ref	Expression
1		alrimih.1	. 2 |- ( ph -> A. x ph )
2		alrimih.2	. . 3 |- ( ph -> ps )
3	2	alimi 1432	. 2 |- ( A. x ph -> A. x ps )
4	1, 3	syl 14	1 |- ( ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1330

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

This theorem is referenced by:  albidh  1457  alrimi  1503  nfd  1504  19.21h  1537  exlimd2  1575  exlimdh  1576  eximdh  1591  nexd  1593  exbidh  1594  hbex  1616  hbnd  1634  19.12  1644  19.38  1655  ax11i  1693  equsalh  1705  nfald  1734  nfexd  1735  aev  1785  equs5or  1803  sb4or  1806  sbbidh  1818  sb6rf  1826  alrimiv  1847  eupicka  2080  2moex  2086