Theorem eximi 1622

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

Syntax hints:   -> wi 4   E.wex 1514

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-ial 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2eximi  1623  eximii  1624  exsimpl  1639  exsimpr  1640  19.29r2  1644  19.29x  1645  19.35-1  1646  19.43  1650  19.40  1653  19.40-2  1654  exanaliim  1669  19.12  1687  equs4  1747  cbvexh  1777  equvini  1780  sbimi  1786  equs5e  1817  exdistrfor  1822  equs45f  1824  sbcof2  1832  sbequi  1861  spsbe  1864  sbidm  1873  cbvexdh  1949  eumo0  2084  mor  2095  euan  2109  eupickb  2134  2eu2ex  2142  2exeu  2145  rexex  2551  reximi2  2601  cgsexg  2806  gencbvex  2818  gencbval  2820  vtocl3  2828  eqvinc  2895  eqvincg  2896  mosubt  2949  rexm  3559  prmg  3753  bm1.3ii  4164  a9evsep  4165  axnul  4168  elrelimasn  5047  dminss  5096  imainss  5097  euiotaex  5247  imadiflem  5352  funimaexglem  5356  brprcneu  5568  fv3  5598  relelfvdm  5607  ssimaex  5639  oprabid  5975  brabvv  5990  uchoice  6222  ecexr  6624  enssdom  6852  fidcenumlemim  7053  subhalfnqq  7526  prarloc  7615  ltexprlemopl  7713  ltexprlemlol  7714  ltexprlemopu  7715  ltexprlemupu  7716  fnpr2ob  13114  fngsum  13162  igsumvalx  13163  bdbm1.3ii  15760  bj-inex  15776  bj-2inf  15807