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  3614  prmg  3820  bm1.3ii  4237  a9evsep  4238  axnul  4241  reldmm  4982  elrelimasn  5135  dminss  5184  imainss  5185  euiotaex  5336  imadiflem  5442  funimaexglem  5446  brprcneu  5670  fv3  5700  relelfvdm  5709  ssimaex  5745  oprabid  6092  brabvv  6109  uchoice  6346  ecexr  6787  enssdom  7016  fidcenumlemim  7237  subhalfnqq  7747  prarloc  7836  ltexprlemopl  7934  ltexprlemlol  7935  ltexprlemopu  7936  ltexprlemupu  7937  fnpr2ob  13610  fngzsum  13657  gzsumvalx  13658  bdbm1.3ii  16802  bj-inex  16818  bj-2inf  16849