Theorem exlimi 1587

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

Syntax hints:   -> wi 4   F/wnf 1453   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1442  ax-ie2 1487  ax-4 1503

This theorem depends on definitions:  df-bi 116  df-nf 1454

This theorem is referenced by:  19.36i  1665  cbvexv1  1745  euexex  2104  ceqsex  2768  sbhypf  2779  vtoclgf  2788  vtoclg1f  2789  vtoclef  2803  copsexg  4227  copsex2g  4229  ralxpf  4755  rexxpf  4756  dmcoss  4878  fv3  5517  tz6.12c  5524  0neqopab  5896  cnvoprab  6211  bj-exlimmpi  13770