MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eximi Structured version   Visualization version   Unicode version

Theorem eximi 1718
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
StepHypRef Expression
1 exim 1717 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1682 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693
This theorem depends on definitions:  df-bi 190  df-ex 1675
This theorem is referenced by:  2eximi  1719  eximii  1720  exa1  1722  exsimpl  1740  exsimpr  1741  19.29r2  1749  19.29x  1750  19.35  1751  19.40-2  1760  exlimiv  1787  speimfwALT  1805  sbimi  1814  19.12  2044  axc9lem2  2144  axc9lem2OLD  2145  exdistrf  2178  equs45f  2192  mo2v  2317  2eu2ex  2386  reximi2  2866  cgsexg  3092  gencbvex  3104  vtocl3  3115  eqvinc  3178  axrep2  4531  bm1.3ii  4542  ax6vsep  4543  axnulOLD  4547  copsexg  4701  dminss  5269  imainss  5270  elsnxp  5397  iotaex  5582  fv3  5901  ssimaex  5953  dffv2  5961  exfo  6063  oprabid  6342  zfrep6  6788  frxp  6933  suppimacnvss  6951  tz7.48-1  7186  enssdom  7620  fineqvlem  7812  infcntss  7871  infeq5  8168  omex  8174  rankuni  8360  scott0  8383  acni3  8504  acnnum  8509  dfac3  8578  dfac9  8592  kmlem1  8606  cflm  8706  cfcof  8730  axdc4lem  8911  axcclem  8913  ac6c4  8937  ac6s  8940  ac6s2  8942  axdclem2  8976  brdom3  8982  brdom5  8983  brdom4  8984  nqpr  9465  ltexprlem4  9490  reclem2pr  9499  hash1to3  12681  trclublem  13108  drsdirfi  16232  2ndcsb  20513  fbssint  20902  isfil2  20920  alexsubALTlem3  21113  lpbl  21567  metustfbas  21621  3v3e3cycl2  25441  ex-natded9.26-2  25919  eqvincg  28157  19.9d2rf  28161  rexunirn  28176  f1ocnt  28425  fmcncfil  28786  esumiun  28964  0elsiga  28985  ddemeas  29108  bnj168  29587  bnj593  29604  bnj607  29776  bnj600  29779  bnj916  29793  fundmpss  30456  exisym1  31133  bj-exlime  31265  bj-nalnaleximiOLD  31267  bj-sbex  31284  bj-ssbequ2  31301  bj-equs45fv  31408  bj-axrep2  31449  bj-eumo0  31488  bj-snsetex  31602  bj-snglss  31609  bj-snglex  31612  bj-ccinftydisj  31700  mptsnunlem  31785  spsbce-2  36774  iotaexeu  36813  iotasbc  36814  relopabVD  37338  ax6e2ndeqVD  37346  2uasbanhVD  37348  ax6e2ndeqALT  37368  fnchoice  37390  rfcnnnub  37397  stoweidlem35  37934  stoweidlem57  37956  n0rex  39028
  Copyright terms: Public domain W3C validator