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  1660  exlimivOLD  1707  19.12  1865  19.12OLD  1866  equs4OLD  1952  ax12olem2  1973  exdistrf  2028  equs45f  2044  sbequi  2108  eumo0  2278  euan  2311  eupickb  2319  2eu2ex  2328  rexex  2725  reximi2  2772  cgsexg  2947  gencbvex  2958  vtocl3  2968  eqvinc  3023  axrep2  4282  bm1.3ii  4293  ax9vsep  4294  axnul  4297  imassrn  5175  dminss  5245  imainss  5246  iotaex  5394  fv3  5703  ssimaex  5747  dffv2  5755  exfo  5846  zfrep6  5927  oprabid  6064  frxp  6415  tz7.48-1  6659  enssdom  7091  fineqvlem  7282  infcntss  7339  infeq5  7548  omex  7554  rankuni  7745  scott0  7766  acni3  7884  finacn  7887  acnnum  7889  dfac3  7958  dfac4  7959  dfac9  7972  kmlem1  7986  kmlem2  7987  cflm  8086  cfcof  8110  axdc4lem  8291  axcclem  8293  ac6c4  8317  ac6c5  8318  ac6s  8320  ac6s2  8322  ac6s3  8323  ac6s5  8327  axdclem2  8356  brdom3  8362  brdom5  8363  brdom4  8364  axpowndlem2  8429  nqpr  8847  ltexprlem4  8872  reclem2pr  8881  drsdirfi  14350  2ndcsb  17465  fbssint  17823  isfil2  17841  alexsubALTlem3  18033  lpbl  18486  metustfbasOLD  18548  metustfbas  18549  3v3e3cycl2  21604  ex-natded9.26-2  21681  eqvincg  23914  19.9d2rf  23921  rexunirn  23931  ceqsexv2d  23938  fmcncfil  24270  0elsiga  24450  fundmpss  25336  exisym1  26078  heiborlem3  26412  exan3  26591  spsbce-2  27447  iotaexeu  27486  iotasbc  27487  fnchoice  27567  rfcnnnub  27574  stoweidlem35  27651  stoweidlem57  27673  relopabVD  28722  a9e2ndeqVD  28730  2uasbanhVD  28732  a9e2ndeqALT  28753  bnj168  28803  bnj593  28819  bnj607  28993  bnj600  28996  bnj916  29010  19.12vAUX7  29160  exdistrfNEW7  29211  equs4NEW7  29237  sbequiNEW7  29282  equs45fNEW7  29322  19.12OLD7  29370
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