Theorem alrimih 1462

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

Syntax hints:   -> wi 4   A.wal 1346

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

This theorem is referenced by:  albidh  1473  alrimi  1515  nfd  1516  19.21h  1550  exlimd2  1588  exlimdh  1589  eximdh  1604  nexd  1606  exbidh  1607  hbex  1629  hbnd  1648  19.12  1658  19.38  1669  ax11i  1707  equsalh  1719  nfald  1753  nfexd  1754  aev  1805  equs5or  1823  sb4or  1826  sbbidh  1838  sb6rf  1846  alrimiv  1867  eupicka  2099  2moex  2105