Theorem eximi 1593

Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eximi.1	|- ( ph -> ps )

Assertion

Ref	Expression
eximi	|- ( E. x ph -> E. x ps )

Proof of Theorem eximi

Step	Hyp	Ref	Expression
1		exim 1592	. 2 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		eximi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1444	1 |- ( E. x ph -> E. x ps )

Syntax hints:   -> wi 4   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximi  1594  eximii  1595  exsimpl  1610  exsimpr  1611  19.29r2  1615  19.29x  1616  19.35-1  1617  19.43  1621  19.40  1624  19.40-2  1625  exanaliim  1640  19.12  1658  equs4  1718  cbvexh  1748  equvini  1751  sbimi  1757  equs5e  1788  exdistrfor  1793  equs45f  1795  sbcof2  1803  sbequi  1832  spsbe  1835  sbidm  1844  cbvexdh  1919  eumo0  2050  mor  2061  euan  2075  eupickb  2100  2eu2ex  2108  2exeu  2111  rexex  2516  reximi2  2566  cgsexg  2765  gencbvex  2776  gencbval  2778  vtocl3  2786  eqvinc  2853  eqvincg  2854  mosubt  2907  rexm  3514  prmg  3704  bm1.3ii  4110  a9evsep  4111  axnul  4114  dminss  5025  imainss  5026  euiotaex  5176  imadiflem  5277  funimaexglem  5281  brprcneu  5489  fv3  5519  relelfvdm  5528  ssimaex  5557  oprabid  5885  brabvv  5899  ecexr  6518  enssdom  6740  fidcenumlemim  6929  subhalfnqq  7376  prarloc  7465  ltexprlemopl  7563  ltexprlemlol  7564  ltexprlemopu  7565  ltexprlemupu  7566  bdbm1.3ii  13926  bj-inex  13942  bj-2inf  13973