Theorem exlimi 1618

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

Syntax hints:   -> wi 4   F/wnf 1484   E.wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1473  ax-ie2 1518  ax-4 1534

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

This theorem is referenced by:  19.36i  1696  cbvexv1  1776  euexex  2141  ceqsex  2815  sbhypf  2827  vtoclgf  2836  vtoclg1f  2837  vtoclef  2853  copsexg  4306  copsex2g  4308  ralxpf  4842  rexxpf  4843  dmcoss  4967  fv3  5622  tz6.12c  5629  0neqopab  6013  cnvoprab  6343  bj-exlimmpi  15906