Theorem eximi 1649

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

Syntax hints:   -> wi 4   E.wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1650  eximii  1651  exsimpl  1666  exsimpr  1667  19.29r2  1671  19.29x  1672  19.35-1  1673  19.43  1677  19.40  1680  19.40-2  1681  exanaliim  1696  19.12  1713  equs4  1773  cbvexh  1804  equvini  1807  sbimi  1813  equs5e  1844  exdistrfor  1849  equs45f  1851  sbcof2  1859  sbequi  1888  spsbe  1891  sbidm  1900  cbvexdh  1976  eumo0  2111  mor  2123  euan  2137  eupickb  2162  2eu2ex  2170  2exeu  2173  rexex  2588  reximi2  2638  cgsexg  2849  gencbvex  2861  gencbval  2863  vtocl3  2871  eqvinc  2940  eqvincg  2941  mosubt  2994  rexm  3609  prmg  3814  bm1.3ii  4231  a9evsep  4232  axnul  4235  reldmm  4975  elrelimasn  5128  dminss  5177  imainss  5178  euiotaex  5329  imadiflem  5435  funimaexglem  5439  brprcneu  5663  fv3  5693  relelfvdm  5702  ssimaex  5738  oprabid  6082  brabvv  6099  uchoice  6331  ecexr  6772  enssdom  7001  fidcenumlemim  7222  subhalfnqq  7729  prarloc  7818  ltexprlemopl  7916  ltexprlemlol  7917  ltexprlemopu  7918  ltexprlemupu  7919  fnpr2ob  13553  fngsum  13601  igsumvalx  13602  bdbm1.3ii  16661  bj-inex  16677  bj-2inf  16708