Theorem eximi 1624

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

Syntax hints:   -> wi 4   E.wex 1516

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1625  eximii  1626  exsimpl  1641  exsimpr  1642  19.29r2  1646  19.29x  1647  19.35-1  1648  19.43  1652  19.40  1655  19.40-2  1656  exanaliim  1671  19.12  1689  equs4  1749  cbvexh  1779  equvini  1782  sbimi  1788  equs5e  1819  exdistrfor  1824  equs45f  1826  sbcof2  1834  sbequi  1863  spsbe  1866  sbidm  1875  cbvexdh  1951  eumo0  2086  mor  2097  euan  2111  eupickb  2136  2eu2ex  2144  2exeu  2147  rexex  2553  reximi2  2603  cgsexg  2809  gencbvex  2821  gencbval  2823  vtocl3  2831  eqvinc  2900  eqvincg  2901  mosubt  2954  rexm  3564  prmg  3760  bm1.3ii  4176  a9evsep  4177  axnul  4180  elrelimasn  5062  dminss  5111  imainss  5112  euiotaex  5262  imadiflem  5367  funimaexglem  5371  brprcneu  5587  fv3  5617  relelfvdm  5626  ssimaex  5658  oprabid  5994  brabvv  6009  uchoice  6241  ecexr  6643  enssdom  6871  fidcenumlemim  7075  subhalfnqq  7557  prarloc  7646  ltexprlemopl  7744  ltexprlemlol  7745  ltexprlemopu  7746  ltexprlemupu  7747  fnpr2ob  13257  fngsum  13305  igsumvalx  13306  bdbm1.3ii  15996  bj-inex  16012  bj-2inf  16043