Theorem eximi 1653

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

Syntax hints:   -> wi 4   E.wex 1545

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1654  eximii  1655  exsimpl  1670  exsimpr  1671  19.29r2  1675  19.29x  1676  19.35-1  1677  19.43  1681  19.40  1684  19.40-2  1685  exanaliim  1700  19.12  1717  equs4  1777  cbvexh  1808  equvini  1811  sbimi  1817  equs5e  1848  exdistrfor  1853  equs45f  1855  sbcof2  1863  sbequi  1892  spsbe  1895  sbidm  1904  cbvexdh  1982  eumo0  2117  mor  2129  euan  2143  eupickb  2168  2eu2ex  2176  2exeu  2179  rexex  2596  reximi2  2646  cgsexg  2857  gencbvex  2869  gencbval  2871  vtocl3  2879  eqvinc  2949  eqvincg  2950  mosubt  3003  rexm  3624  prmg  3830  bm1.3ii  4249  a9evsep  4250  axnul  4253  reldmm  4995  elrelimasn  5148  dminss  5197  imainss  5198  euiotaex  5349  imadiflem  5455  funimaexglem  5459  brprcneu  5683  fv3  5713  relelfvdm  5722  ssimaex  5758  oprabid  6107  brabvv  6124  uchoice  6361  ecexr  6802  enssdom  7038  fidcenumlemim  7259  subhalfnqq  7771  prarloc  7860  ltexprlemopl  7958  ltexprlemlol  7959  ltexprlemopu  7960  ltexprlemupu  7961  fnpr2ob  13638  fngzsum  13685  gzsumvalx  13686  bdbm1.3ii  16831  bj-inex  16847  bj-2inf  16878