Theorem eximi 1611

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

Syntax hints:   -> wi 4   E.wex 1503

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1612  eximii  1613  exsimpl  1628  exsimpr  1629  19.29r2  1633  19.29x  1634  19.35-1  1635  19.43  1639  19.40  1642  19.40-2  1643  exanaliim  1658  19.12  1676  equs4  1736  cbvexh  1766  equvini  1769  sbimi  1775  equs5e  1806  exdistrfor  1811  equs45f  1813  sbcof2  1821  sbequi  1850  spsbe  1853  sbidm  1862  cbvexdh  1938  eumo0  2069  mor  2080  euan  2094  eupickb  2119  2eu2ex  2127  2exeu  2130  rexex  2536  reximi2  2586  cgsexg  2791  gencbvex  2802  gencbval  2804  vtocl3  2812  eqvinc  2879  eqvincg  2880  mosubt  2933  rexm  3541  prmg  3735  bm1.3ii  4146  a9evsep  4147  axnul  4150  elrelimasn  5019  dminss  5068  imainss  5069  euiotaex  5219  imadiflem  5321  funimaexglem  5325  brprcneu  5534  fv3  5564  relelfvdm  5573  ssimaex  5605  oprabid  5936  brabvv  5950  ecexr  6572  enssdom  6796  fidcenumlemim  6990  subhalfnqq  7453  prarloc  7542  ltexprlemopl  7640  ltexprlemlol  7641  ltexprlemopu  7642  ltexprlemupu  7643  fnpr2ob  12834  fngsum  12882  igsumvalx  12883  bdbm1.3ii  15182  bj-inex  15198  bj-2inf  15229