Theorem eximi 1648

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

Syntax hints:   -> wi 4   E.wex 1540

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1649  eximii  1650  exsimpl  1665  exsimpr  1666  19.29r2  1670  19.29x  1671  19.35-1  1672  19.43  1676  19.40  1679  19.40-2  1680  exanaliim  1695  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  2578  reximi2  2628  cgsexg  2838  gencbvex  2850  gencbval  2852  vtocl3  2860  eqvinc  2929  eqvincg  2930  mosubt  2983  rexm  3594  prmg  3794  bm1.3ii  4210  a9evsep  4211  axnul  4214  reldmm  4950  elrelimasn  5102  dminss  5151  imainss  5152  euiotaex  5303  imadiflem  5409  funimaexglem  5413  brprcneu  5632  fv3  5662  relelfvdm  5671  ssimaex  5707  oprabid  6049  brabvv  6066  uchoice  6299  ecexr  6706  enssdom  6934  fidcenumlemim  7150  subhalfnqq  7633  prarloc  7722  ltexprlemopl  7820  ltexprlemlol  7821  ltexprlemopu  7822  ltexprlemupu  7823  fnpr2ob  13422  fngsum  13470  igsumvalx  13471  bdbm1.3ii  16486  bj-inex  16502  bj-2inf  16533