Theorem exlimi 1640

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 1565	. 2 |- ( ps -> A. x ps )
3		exlimi.2	. 2 |- ( ph -> ps )
4	2, 3	exlimih 1639	1 |- ( E. x ph -> ps )

Syntax hints:   -> wi 4   F/wnf 1506   E.wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1495  ax-ie2 1540  ax-4 1556

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

This theorem is referenced by:  19.36i  1718  cbvexv1  1798  euexex  2163  ceqsex  2838  sbhypf  2850  vtoclgf  2859  vtoclg1f  2860  vtoclef  2876  copsexg  4330  copsex2g  4332  ralxpf  4868  rexxpf  4869  dmcoss  4994  fv3  5650  tz6.12c  5657  0neqopab  6049  cnvoprab  6380  bj-exlimmpi  16134