Theorem alrimih 1398

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

Syntax hints:   -> wi 4   A.wal 1282

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

This theorem is referenced by:  albidh  1409  alrimi  1455  nfd  1456  19.21h  1489  exlimd2  1526  exlimdh  1527  eximdh  1542  nexd  1544  exbidh  1545  hbex  1567  hbnd  1585  19.12  1595  19.38  1606  ax11i  1642  equsalh  1654  nfald  1683  nfexd  1684  aev  1733  equs5or  1751  sb4or  1754  sbbidh  1766  sb6rf  1774  alrimiv  1795  eupicka  2021  2moex  2027