Theorem alrimih 1457

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

Syntax hints:   -> wi 4   A.wal 1341

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

This theorem is referenced by:  albidh  1468  alrimi  1510  nfd  1511  19.21h  1545  exlimd2  1583  exlimdh  1584  eximdh  1599  nexd  1601  exbidh  1602  hbex  1624  hbnd  1643  19.12  1653  19.38  1664  ax11i  1702  equsalh  1714  nfald  1748  nfexd  1749  aev  1800  equs5or  1818  sb4or  1821  sbbidh  1833  sb6rf  1841  alrimiv  1862  eupicka  2094  2moex  2100