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  4254  a9evsep  4255  axnul  4258  reldmm  5000  elrelimasn  5153  dminss  5202  imainss  5203  euiotaex  5354  imadiflem  5460  funimaexglem  5464  brprcneu  5688  fv3  5718  relelfvdm  5727  ssimaex  5764  mptmex  5945  oprabid  6117  brabvv  6134  uchoice  6371  ecexr  6812  enssdom  7048  fidcenumlemim  7269  subhalfnqq  7781  prarloc  7870  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  fnpr2ob  13661  fngzsum  13708  gzsumvalx  13709  bdbm1.3ii  16917  bj-inex  16933  bj-2inf  16964