Theorem exlimi 1617

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
exlimi.1	|- F/ x ps
exlimi.2	|- ( ph -> ps )

Assertion

Ref	Expression
exlimi	|- ( E. x ph -> ps )

Proof of Theorem exlimi

Step	Hyp	Ref	Expression
1		exlimi.1	. . 3 |- F/ x ps
2	1	nfri 1542	. 2 |- ( ps -> A. x ps )
3		exlimi.2	. 2 |- ( ph -> ps )
4	2, 3	exlimih 1616	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   F/wnf 1483   E.wex 1515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1472  ax-ie2 1517  ax-4 1533

This theorem depends on definitions:  df-bi 117  df-nf 1484

This theorem is referenced by:  19.36i  1695  cbvexv1  1775  euexex  2139  ceqsex  2810  sbhypf  2822  vtoclgf  2831  vtoclg1f  2832  vtoclef  2846  copsexg  4289  copsex2g  4291  ralxpf  4825  rexxpf  4826  dmcoss  4949  fv3  5601  tz6.12c  5608  0neqopab  5992  cnvoprab  6322  bj-exlimmpi  15743