Theorem alrimih 1483

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

Syntax hints:   -> wi 4   A.wal 1362

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

This theorem is referenced by:  albidh  1494  alrimi  1536  nfd  1537  19.21h  1571  exlimd2  1609  exlimdh  1610  eximdh  1625  nexd  1627  exbidh  1628  hbex  1650  hbnd  1669  19.12  1679  19.38  1690  ax11i  1728  equsalh  1740  nfald  1774  nfexd  1775  aev  1826  equs5or  1844  sb4or  1847  sbbidh  1859  sb6rf  1867  alrimiv  1888  eupicka  2125  2moex  2131