Theorem eximi 1614

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

Syntax hints:   -> wi 4   E.wex 1506

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1615  eximii  1616  exsimpl  1631  exsimpr  1632  19.29r2  1636  19.29x  1637  19.35-1  1638  19.43  1642  19.40  1645  19.40-2  1646  exanaliim  1661  19.12  1679  equs4  1739  cbvexh  1769  equvini  1772  sbimi  1778  equs5e  1809  exdistrfor  1814  equs45f  1816  sbcof2  1824  sbequi  1853  spsbe  1856  sbidm  1865  cbvexdh  1941  eumo0  2076  mor  2087  euan  2101  eupickb  2126  2eu2ex  2134  2exeu  2137  rexex  2543  reximi2  2593  cgsexg  2798  gencbvex  2810  gencbval  2812  vtocl3  2820  eqvinc  2887  eqvincg  2888  mosubt  2941  rexm  3550  prmg  3743  bm1.3ii  4154  a9evsep  4155  axnul  4158  elrelimasn  5035  dminss  5084  imainss  5085  euiotaex  5235  imadiflem  5337  funimaexglem  5341  brprcneu  5551  fv3  5581  relelfvdm  5590  ssimaex  5622  oprabid  5954  brabvv  5968  uchoice  6195  ecexr  6597  enssdom  6821  fidcenumlemim  7018  subhalfnqq  7481  prarloc  7570  ltexprlemopl  7668  ltexprlemlol  7669  ltexprlemopu  7670  ltexprlemupu  7671  fnpr2ob  12983  fngsum  13031  igsumvalx  13032  bdbm1.3ii  15537  bj-inex  15553  bj-2inf  15584