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  2776  sbhypf  2787  vtoclgf  2796  vtoclg1f  2797  vtoclef  2811  copsexg  4245  copsex2g  4247  ralxpf  4774  rexxpf  4775  dmcoss  4897  fv3  5539  tz6.12c  5546  0neqopab  5920  cnvoprab  6235  bj-exlimmpi  14525