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 )

This proof depends on syntax axioms:   -> wi 4   E.wex 1545

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used 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  3627  prmg  3835  bm1.3ii  4256  a9evsep  4257  axnul  4260  reldmm  5002  elrelimasn  5156  dminss  5205  imainss  5206  euiotaex  5357  imadiflem  5463  funimaexglem  5467  brprcneu  5691  fv3  5721  relelfvdm  5730  ssimaex  5767  mptmex  5948  oprabid  6120  brabvv  6137  uchoice  6375  ecexr  6816  enssdom  7052  fidcenumlemim  7274  subhalfnqq  7787  prarloc  7876  ltexprlemopl  7974  ltexprlemlol  7975  ltexprlemopu  7976  ltexprlemupu  7977  fnpr2ob  13720  fngzsum  13767  gzsumvalx  13768  bdbm1.3ii  17122  bj-inex  17138  bj-2inf  17169