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

Theorem eximi 1586
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
StepHypRef Expression
1 exim 1585 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1558 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1551
This theorem is referenced by:  2eximi  1587  eximii  1588  exsimpl  1603  19.29r2  1609  19.29x  1610  19.40  1620  19.40-2  1621  exlimiv  1645  speimfw  1656  spsbe  1664  sbimi  1665  exlimivOLD  1712  19.12  1870  19.12OLD  1871  equs4OLD  1999  ax12olem2  2007  exdistrf  2067  exdistrfOLD  2068  equs45f  2089  sbequi  2112  sbequiOLD  2116  eumo0  2307  euan  2340  eupickb  2348  2eu2ex  2357  rexex  2767  reximi2  2814  cgsexg  2989  gencbvex  3000  vtocl3  3010  eqvinc  3065  axrep2  4325  bm1.3ii  4336  ax9vsep  4337  axnul  4340  imassrn  5219  dminss  5289  imainss  5290  iotaex  5438  fv3  5747  ssimaex  5791  dffv2  5799  exfo  5890  zfrep6  5971  oprabid  6108  frxp  6459  tz7.48-1  6703  enssdom  7135  fineqvlem  7326  infcntss  7383  infeq5  7595  omex  7601  rankuni  7792  scott0  7815  acni3  7933  finacn  7936  acnnum  7938  dfac3  8007  dfac4  8008  dfac9  8021  kmlem1  8035  kmlem2  8036  cflm  8135  cfcof  8159  axdc4lem  8340  axcclem  8342  ac6c4  8366  ac6c5  8367  ac6s  8369  ac6s2  8371  ac6s3  8372  ac6s5  8376  axdclem2  8405  brdom3  8411  brdom5  8412  brdom4  8413  axpowndlem2  8478  nqpr  8896  ltexprlem4  8921  reclem2pr  8930  drsdirfi  14400  2ndcsb  17517  fbssint  17875  isfil2  17893  alexsubALTlem3  18085  lpbl  18538  metustfbasOLD  18600  metustfbas  18601  3v3e3cycl2  21656  ex-natded9.26-2  21733  eqvincg  23966  19.9d2rf  23973  rexunirn  23983  ceqsexv2d  23990  fmcncfil  24322  0elsiga  24502  fundmpss  25395  exisym1  26179  heiborlem3  26536  exan3  26715  spsbce-2  27570  iotaexeu  27609  iotasbc  27610  fnchoice  27690  rfcnnnub  27697  stoweidlem35  27774  stoweidlem57  27796  relopabVD  29087  a9e2ndeqVD  29095  2uasbanhVD  29097  a9e2ndeqALT  29117  bnj168  29171  bnj593  29187  bnj607  29361  bnj600  29364  bnj916  29378  19.12vAUX7  29528  exdistrfNEW7  29579  equs4NEW7  29607  sbequiNEW7  29653  equs45fNEW7  29695  19.12OLD7  29760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator