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

Theorem eximi 1582
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 1581 . 2  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
2 eximi.1 . 2  |-  ( ph  ->  ps )
31, 2mpg 1554 1  |-  ( E. x ph  ->  E. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1547
This theorem is referenced by:  2eximi  1583  eximii  1584  exsimpl  1599  19.29r2  1605  19.29x  1606  19.40  1616  19.40-2  1617  exlimiv  1641  speimfw  1652  sbimi  1659  exlimivOLD  1705  19.12  1859  19.12OLD  1860  equs4OLD  1945  ax12olem2  1966  exdistrf  2015  equs45f  2029  sbequi  2094  eumo0  2264  euan  2297  eupickb  2305  2eu2ex  2314  rexex  2710  reximi2  2757  cgsexg  2932  gencbvex  2943  vtocl3  2953  eqvinc  3008  axrep2  4265  bm1.3ii  4276  ax9vsep  4277  axnul  4280  imassrn  5158  dminss  5228  imainss  5229  iotaex  5377  fv3  5686  ssimaex  5729  dffv2  5737  exfo  5828  zfrep6  5909  oprabid  6046  frxp  6394  tz7.48-1  6638  enssdom  7070  fineqvlem  7261  infcntss  7318  infeq5  7527  omex  7533  rankuni  7724  scott0  7745  acni3  7863  finacn  7866  acnnum  7868  dfac3  7937  dfac4  7938  dfac9  7951  kmlem1  7965  kmlem2  7966  cflm  8065  cfcof  8089  axdc4lem  8270  axcclem  8272  ac6c4  8296  ac6c5  8297  ac6s  8299  ac6s2  8301  ac6s3  8302  ac6s5  8306  axdclem2  8335  brdom3  8341  brdom5  8342  brdom4  8343  axpowndlem2  8408  nqpr  8826  ltexprlem4  8851  reclem2pr  8860  drsdirfi  14324  2ndcsb  17435  fbssint  17793  isfil2  17811  alexsubALTlem3  18003  lpbl  18425  metustfbas  18479  3v3e3cycl2  21501  ex-natded9.26-2  21578  eqvincg  23807  19.9d2rf  23814  rexunirn  23824  ceqsexv2d  23831  fmcncfil  24123  0elsiga  24295  fundmpss  25148  exisym1  25890  heiborlem3  26215  exan3  26394  spsbce-2  27250  iotaexeu  27289  iotasbc  27290  fnchoice  27370  rfcnnnub  27377  stoweidlem35  27454  stoweidlem57  27476  relopabVD  28356  a9e2ndeqVD  28364  2uasbanhVD  28366  a9e2ndeqALT  28387  bnj168  28437  bnj593  28453  bnj607  28627  bnj600  28630  bnj916  28644  19.12vAUX7  28794  exdistrfNEW7  28845  equs4NEW7  28871  sbequiNEW7  28916  equs45fNEW7  28956  19.12OLD7  29004
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator