Theorem eximi 1623

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

Syntax hints:   -> wi 4   E.wex 1515

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1624  eximii  1625  exsimpl  1640  exsimpr  1641  19.29r2  1645  19.29x  1646  19.35-1  1647  19.43  1651  19.40  1654  19.40-2  1655  exanaliim  1670  19.12  1688  equs4  1748  cbvexh  1778  equvini  1781  sbimi  1787  equs5e  1818  exdistrfor  1823  equs45f  1825  sbcof2  1833  sbequi  1862  spsbe  1865  sbidm  1874  cbvexdh  1950  eumo0  2085  mor  2096  euan  2110  eupickb  2135  2eu2ex  2143  2exeu  2146  rexex  2552  reximi2  2602  cgsexg  2807  gencbvex  2819  gencbval  2821  vtocl3  2829  eqvinc  2896  eqvincg  2897  mosubt  2950  rexm  3560  prmg  3754  bm1.3ii  4165  a9evsep  4166  axnul  4169  elrelimasn  5048  dminss  5097  imainss  5098  euiotaex  5248  imadiflem  5353  funimaexglem  5357  brprcneu  5569  fv3  5599  relelfvdm  5608  ssimaex  5640  oprabid  5976  brabvv  5991  uchoice  6223  ecexr  6625  enssdom  6853  fidcenumlemim  7054  subhalfnqq  7527  prarloc  7616  ltexprlemopl  7714  ltexprlemlol  7715  ltexprlemopu  7716  ltexprlemupu  7717  fnpr2ob  13172  fngsum  13220  igsumvalx  13221  bdbm1.3ii  15827  bj-inex  15843  bj-2inf  15874