Theorem eximi 1646

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

Syntax hints:   -> wi 4   E.wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1647  eximii  1648  exsimpl  1663  exsimpr  1664  19.29r2  1668  19.29x  1669  19.35-1  1670  19.43  1674  19.40  1677  19.40-2  1678  exanaliim  1693  19.12  1711  equs4  1771  cbvexh  1801  equvini  1804  sbimi  1810  equs5e  1841  exdistrfor  1846  equs45f  1848  sbcof2  1856  sbequi  1885  spsbe  1888  sbidm  1897  cbvexdh  1973  eumo0  2108  mor  2120  euan  2134  eupickb  2159  2eu2ex  2167  2exeu  2170  rexex  2576  reximi2  2626  cgsexg  2835  gencbvex  2847  gencbval  2849  vtocl3  2857  eqvinc  2926  eqvincg  2927  mosubt  2980  rexm  3591  prmg  3788  bm1.3ii  4204  a9evsep  4205  axnul  4208  reldmm  4941  elrelimasn  5093  dminss  5142  imainss  5143  euiotaex  5294  imadiflem  5399  funimaexglem  5403  brprcneu  5619  fv3  5649  relelfvdm  5658  ssimaex  5694  oprabid  6032  brabvv  6049  uchoice  6281  ecexr  6683  enssdom  6911  fidcenumlemim  7115  subhalfnqq  7597  prarloc  7686  ltexprlemopl  7784  ltexprlemlol  7785  ltexprlemopu  7786  ltexprlemupu  7787  fnpr2ob  13368  fngsum  13416  igsumvalx  13417  bdbm1.3ii  16212  bj-inex  16228  bj-2inf  16259