Theorem alrimih 1358

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

Syntax hints:   -> wi 4   A.wal 1241

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

This theorem is referenced by:  albidh  1369  alrimi  1415  nfd  1416  19.21h  1449  exlimd2  1486  exlimdh  1487  eximdh  1502  nexd  1504  exbidh  1505  hbex  1527  hbnd  1545  19.12  1555  19.38  1566  ax11i  1602  equsalh  1614  nfald  1643  nfexd  1644  aev  1693  equs5or  1711  sb4or  1714  sbbid  1726  sb6rf  1733  alrimiv  1754  eupicka  1980  2moex  1986