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  4288  copsex2g  4290  ralxpf  4824  rexxpf  4825  dmcoss  4948  fv3  5599  tz6.12c  5606  0neqopab  5990  cnvoprab  6320  bj-exlimmpi  15706