Theorem alrimih 1469

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

Syntax hints:   -> wi 4   A.wal 1351

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

This theorem is referenced by:  albidh  1480  alrimi  1522  nfd  1523  19.21h  1557  exlimd2  1595  exlimdh  1596  eximdh  1611  nexd  1613  exbidh  1614  hbex  1636  hbnd  1655  19.12  1665  19.38  1676  ax11i  1714  equsalh  1726  nfald  1760  nfexd  1761  aev  1812  equs5or  1830  sb4or  1833  sbbidh  1845  sb6rf  1853  alrimiv  1874  eupicka  2106  2moex  2112