Theorem alrimih 1445

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

Syntax hints:   -> wi 4   A.wal 1329

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

This theorem is referenced by:  albidh  1456  alrimi  1502  nfd  1503  19.21h  1536  exlimd2  1574  exlimdh  1575  eximdh  1590  nexd  1592  exbidh  1593  hbex  1615  hbnd  1633  19.12  1643  19.38  1654  ax11i  1692  equsalh  1704  nfald  1733  nfexd  1734  aev  1784  equs5or  1802  sb4or  1805  sbbidh  1817  sb6rf  1825  alrimiv  1846  eupicka  2079  2moex  2085