Theorem alrimih 1522

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 1508	. 2 |- ( A. x ph -> A. x ps )
4	1, 3	syl 14	1 |- ( ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1400

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

This theorem is referenced by:  albidh  1533  alrimi  1575  nfd  1576  19.21h  1610  exlimd2  1648  exlimdh  1649  eximdh  1664  nexd  1666  exbidh  1667  hbex  1689  hbnd  1707  19.12  1717  19.38  1728  ax11i  1766  equsalh  1778  nfald  1813  nfexd  1814  aev  1865  equs5or  1883  sb4or  1886  sbbidh  1898  sb6rf  1906  alrimiv  1927  eupicka  2167  2moex  2173