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  1803  equvini  1806  sbimi  1812  equs5e  1843  exdistrfor  1848  equs45f  1850  sbcof2  1858  sbequi  1887  spsbe  1890  sbidm  1899  cbvexdh  1975  eumo0  2110  mor  2122  euan  2136  eupickb  2161  2eu2ex  2169  2exeu  2172  rexex  2579  reximi2  2629  cgsexg  2839  gencbvex  2851  gencbval  2853  vtocl3  2861  eqvinc  2930  eqvincg  2931  mosubt  2984  rexm  3596  prmg  3798  bm1.3ii  4215  a9evsep  4216  axnul  4219  reldmm  4956  elrelimasn  5109  dminss  5158  imainss  5159  euiotaex  5310  imadiflem  5416  funimaexglem  5420  brprcneu  5641  fv3  5671  relelfvdm  5680  ssimaex  5716  oprabid  6060  brabvv  6077  uchoice  6309  ecexr  6750  enssdom  6978  fidcenumlemim  7194  subhalfnqq  7677  prarloc  7766  ltexprlemopl  7864  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  fnpr2ob  13486  fngsum  13534  igsumvalx  13535  bdbm1.3ii  16590  bj-inex  16606  bj-2inf  16637