Theorem exlimi 1608

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

Syntax hints:   -> wi 4   F/wnf 1474   E.wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1463  ax-ie2 1508  ax-4 1524

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

This theorem is referenced by:  19.36i  1686  cbvexv1  1766  euexex  2130  ceqsex  2801  sbhypf  2813  vtoclgf  2822  vtoclg1f  2823  vtoclef  2837  copsexg  4278  copsex2g  4280  ralxpf  4813  rexxpf  4814  dmcoss  4936  fv3  5584  tz6.12c  5591  0neqopab  5971  cnvoprab  6301  bj-exlimmpi  15500