Theorem exlimi 1647

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

This proof depends on syntax axioms:   -> wi 4   F/wnf 1513   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-4 1563

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  19.36i  1724  cbvexv1  1805  euexex  2172  ceqsex  2860  sbhypf  2872  vtoclgf  2881  vtoclg1f  2882  vtoclef  2898  copsexg  4386  copsex2g  4388  ralxpf  4928  rexxpf  4929  dmcoss  5054  fv3  5721  tz6.12c  5728  0neqopab  6136  cnvoprab  6474  bj-exlimmpi  17003