Theorem exlimi 1643

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

Syntax hints:   -> wi 4   F/wnf 1509   E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-4 1559

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

This theorem is referenced by:  19.36i  1720  cbvexv1  1801  euexex  2166  ceqsex  2852  sbhypf  2864  vtoclgf  2873  vtoclg1f  2874  vtoclef  2890  copsexg  4360  copsex2g  4362  ralxpf  4901  rexxpf  4902  dmcoss  5027  fv3  5693  tz6.12c  5700  0neqopab  6098  cnvoprab  6430  bj-exlimmpi  16542