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  2836  gencbvex  2848  gencbval  2850  vtocl3  2858  eqvinc  2927  eqvincg  2928  mosubt  2981  rexm  3592  prmg  3792  bm1.3ii  4208  a9evsep  4209  axnul  4212  reldmm  4948  elrelimasn  5100  dminss  5149  imainss  5150  euiotaex  5301  imadiflem  5406  funimaexglem  5410  brprcneu  5628  fv3  5658  relelfvdm  5667  ssimaex  5703  oprabid  6045  brabvv  6062  uchoice  6295  ecexr  6702  enssdom  6930  fidcenumlemim  7142  subhalfnqq  7624  prarloc  7713  ltexprlemopl  7811  ltexprlemlol  7812  ltexprlemopu  7813  ltexprlemupu  7814  fnpr2ob  13413  fngsum  13461  igsumvalx  13462  bdbm1.3ii  16422  bj-inex  16438  bj-2inf  16469