Theorem exlimi 1573

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

Syntax hints:   -> wi 4   F/wnf 1436   E.wex 1468

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

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

This theorem is referenced by:  19.36i  1650  euexex  2084  ceqsex  2724  sbhypf  2735  vtoclgf  2744  vtoclg1f  2745  vtoclef  2759  copsexg  4166  copsex2g  4168  ralxpf  4685  rexxpf  4686  dmcoss  4808  fv3  5444  tz6.12c  5451  0neqopab  5816  cnvoprab  6131  bj-exlimmpi  12977