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  4277  copsex2g  4279  ralxpf  4812  rexxpf  4813  dmcoss  4935  fv3  5581  tz6.12c  5588  0neqopab  5967  cnvoprab  6292  bj-exlimmpi  15416