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  2073  mor  2084  euan  2098  eupickb  2123  2eu2ex  2131  2exeu  2134  rexex  2540  reximi2  2590  cgsexg  2795  gencbvex  2806  gencbval  2808  vtocl3  2816  eqvinc  2883  eqvincg  2884  mosubt  2937  rexm  3546  prmg  3739  bm1.3ii  4150  a9evsep  4151  axnul  4154  elrelimasn  5031  dminss  5080  imainss  5081  euiotaex  5231  imadiflem  5333  funimaexglem  5337  brprcneu  5547  fv3  5577  relelfvdm  5586  ssimaex  5618  oprabid  5950  brabvv  5964  uchoice  6190  ecexr  6592  enssdom  6816  fidcenumlemim  7011  subhalfnqq  7474  prarloc  7563  ltexprlemopl  7661  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  fnpr2ob  12923  fngsum  12971  igsumvalx  12972  bdbm1.3ii  15383  bj-inex  15399  bj-2inf  15430