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  2082  ceqsex  2719  sbhypf  2730  vtoclgf  2739  vtoclg1f  2740  vtoclef  2754  copsexg  4161  copsex2g  4163  ralxpf  4680  rexxpf  4681  dmcoss  4803  fv3  5437  tz6.12c  5444  0neqopab  5809  cnvoprab  6124  bj-exlimmpi  12966