Theorem eximi 1762

Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-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 1761	. 2 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		eximi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1724	1 |- ( E. x ph -> E. x ps )

Syntax hints:   -> wi 4   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  2eximi  1763  eximii  1764  exa1  1765  exan  1788  exsimpl  1795  exsimpr  1796  19.29r2  1803  19.29x  1804  19.35  1805  19.40-2  1814  exlimiv  1858  speimfwALT  1877  sbimi  1886  19.12  2164  ax13lem2  2296  exdistrf  2333  equs45f  2350  mo2v  2477  2eu2ex  2546  reximi2  3010  cgsexg  3238  gencbvex  3250  vtocl3  3262  eqvincg  3329  n0rex  3935  axrep2  4773  bm1.3ii  4784  ax6vsep  4785  copsexg  4956  relopabi  5245  dminss  5547  imainss  5548  elsnxpOLD  5678  iotaex  5868  fv3  6206  ssimaex  6263  dffv2  6271  exfo  6377  oprabid  6677  zfrep6  7134  frxp  7287  suppimacnvss  7305  tz7.48-1  7538  enssdom  7980  fineqvlem  8174  infcntss  8234  infeq5  8534  omex  8540  rankuni  8726  scott0  8749  acni3  8870  acnnum  8875  dfac3  8944  dfac9  8958  kmlem1  8972  cflm  9072  cfcof  9096  axdc4lem  9277  axcclem  9279  ac6c4  9303  ac6s  9306  ac6s2  9308  axdclem2  9342  brdom3  9350  brdom5  9351  brdom4  9352  nqpr  9836  ltexprlem4  9861  reclem2pr  9870  hash1to3  13273  trclublem  13734  drsdirfi  16938  toprntopon  20729  2ndcsb  21252  fbssint  21642  isfil2  21660  alexsubALTlem3  21853  lpbl  22308  metustfbas  22362  ex-natded9.26-2  27277  19.9d2rf  29318  rexunirn  29331  f1ocnt  29559  fsumiunle  29575  fmcncfil  29977  esumiun  30156  0elsiga  30177  ddemeas  30299  bnj168  30798  bnj593  30815  bnj607  30986  bnj600  30989  bnj916  31003  fundmpss  31664  exisym1  32423  bj-exlime  32609  bj-sbex  32626  bj-ssbequ2  32643  bj-equs45fv  32752  bj-axrep2  32789  bj-eumo0  32830  bj-snsetex  32951  bj-snglss  32958  bj-snglex  32961  bj-restn0  33043  bj-ccinftydisj  33100  mptsnunlem  33185  spsbce-2  38580  iotaexeu  38619  iotasbc  38620  relopabVD  39137  ax6e2ndeqVD  39145  2uasbanhVD  39147  ax6e2ndeqALT  39167  fnchoice  39188  rfcnnnub  39195  stoweidlem35  40252  stoweidlem57  40274