Theorem exlimi 1594

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

Syntax hints:   -> wi 4   F/wnf 1460   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1449  ax-ie2 1494  ax-4 1510

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

This theorem is referenced by:  19.36i  1672  cbvexv1  1752  euexex  2111  ceqsex  2775  sbhypf  2786  vtoclgf  2795  vtoclg1f  2796  vtoclef  2810  copsexg  4244  copsex2g  4246  ralxpf  4773  rexxpf  4774  dmcoss  4896  fv3  5538  tz6.12c  5545  0neqopab  5919  cnvoprab  6234  bj-exlimmpi  14492