Theorem alrimih 1449

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

Syntax hints:   -> wi 4   A.wal 1333

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

This theorem is referenced by:  albidh  1460  alrimi  1502  nfd  1503  19.21h  1537  exlimd2  1575  exlimdh  1576  eximdh  1591  nexd  1593  exbidh  1594  hbex  1616  hbnd  1635  19.12  1645  19.38  1656  ax11i  1694  equsalh  1706  nfald  1740  nfexd  1741  aev  1792  equs5or  1810  sb4or  1813  sbbidh  1825  sb6rf  1833  alrimiv  1854  eupicka  2086  2moex  2092