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  1978  eumo0  2113  mor  2125  euan  2139  eupickb  2164  2eu2ex  2172  2exeu  2175  rexex  2590  reximi2  2640  cgsexg  2851  gencbvex  2863  gencbval  2865  vtocl3  2873  eqvinc  2943  eqvincg  2944  mosubt  2997  rexm  3613  prmg  3819  bm1.3ii  4236  a9evsep  4237  axnul  4240  reldmm  4980  elrelimasn  5133  dminss  5182  imainss  5183  euiotaex  5334  imadiflem  5440  funimaexglem  5444  brprcneu  5668  fv3  5698  relelfvdm  5707  ssimaex  5743  oprabid  6090  brabvv  6107  uchoice  6344  ecexr  6785  enssdom  7014  fidcenumlemim  7235  subhalfnqq  7745  prarloc  7834  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  fnpr2ob  13604  fngsum  13651  igsumvalx  13652  bdbm1.3ii  16787  bj-inex  16803  bj-2inf  16834