Theorem eximi 1531

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

Syntax hints:   -> wi 4   E.wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  2eximi  1532  eximii  1533  exsimpl  1548  exsimpr  1549  19.29r2  1553  19.29x  1554  19.35-1  1555  19.43  1559  19.40  1562  19.40-2  1563  exanaliim  1578  19.12  1595  equs4  1653  cbvexh  1678  equvini  1681  sbimi  1687  equs5e  1716  exdistrfor  1721  equs45f  1723  sbcof2  1731  sbequi  1760  spsbe  1763  sbidm  1772  cbvexdh  1842  eumo0  1972  mor  1983  euan  1997  eupickb  2022  2eu2ex  2030  2exeu  2033  rexex  2410  reximi2  2457  cgsexg  2634  gencbvex  2645  gencbval  2647  vtocl3  2655  eqvinc  2718  eqvincg  2719  mosubt  2769  rexm  3340  prmg  3511  bm1.3ii  3899  a9evsep  3900  axnul  3903  dminss  4758  imainss  4759  euiotaex  4903  imadiflem  4998  funimaexglem  5002  brprcneu  5191  fv3  5218  relelfvdm  5226  ssimaex  5255  oprabid  5557  brabvv  5571  ecexr  6134  enssdom  6265  subhalfnqq  6604  prarloc  6693  ltexprlemopl  6791  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  bdbm1.3ii  10682  bj-inex  10698  bj-2inf  10733