Theorem eximi 1562

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 1561	. 2 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		eximi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1410	1 |- ( E. x ph -> E. x ps )

Syntax hints:   -> wi 4   E.wex 1451

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2eximi  1563  eximii  1564  exsimpl  1579  exsimpr  1580  19.29r2  1584  19.29x  1585  19.35-1  1586  19.43  1590  19.40  1593  19.40-2  1594  exanaliim  1609  19.12  1626  equs4  1686  cbvexh  1711  equvini  1714  sbimi  1720  equs5e  1749  exdistrfor  1754  equs45f  1756  sbcof2  1764  sbequi  1793  spsbe  1796  sbidm  1805  cbvexdh  1876  eumo0  2006  mor  2017  euan  2031  eupickb  2056  2eu2ex  2064  2exeu  2067  rexex  2453  reximi2  2502  cgsexg  2692  gencbvex  2703  gencbval  2705  vtocl3  2713  eqvinc  2778  eqvincg  2779  mosubt  2830  rexm  3428  prmg  3610  bm1.3ii  4009  a9evsep  4010  axnul  4013  dminss  4911  imainss  4912  euiotaex  5062  imadiflem  5160  funimaexglem  5164  brprcneu  5368  fv3  5398  relelfvdm  5407  ssimaex  5436  oprabid  5757  brabvv  5771  ecexr  6388  enssdom  6610  fidcenumlemim  6792  subhalfnqq  7170  prarloc  7259  ltexprlemopl  7357  ltexprlemlol  7358  ltexprlemopu  7359  ltexprlemupu  7360  bdbm1.3ii  12779  bj-inex  12795  bj-2inf  12826