Theorem alrimih 1399

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

Syntax hints:   -> wi 4   A.wal 1283

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

This theorem is referenced by:  albidh  1410  alrimi  1456  nfd  1457  19.21h  1490  exlimd2  1527  exlimdh  1528  eximdh  1543  nexd  1545  exbidh  1546  hbex  1568  hbnd  1586  19.12  1596  19.38  1607  ax11i  1643  equsalh  1655  nfald  1684  nfexd  1685  aev  1734  equs5or  1752  sb4or  1755  sbbidh  1767  sb6rf  1775  alrimiv  1796  eupicka  2022  2moex  2028