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

Theorem eximi 1618
Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eximi.1
Assertion
Ref Expression
eximi

Proof of Theorem eximi
StepHypRef Expression
1 exim 1617 . 2
2 eximi.1 . 2
31, 2mpg 1588 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1581
This theorem is referenced by:  2eximi  1619  eximii  1620  exsimpl  1636  exsimpr  1637  19.29r2  1643  19.29x  1644  19.40-2  1655  exlimiv  1679  speimfw  1690  sbimi  1699  19.12  1866  axc9lem2  1979  exdistrf  2016  equs45f  2032  mo2v  2250  eumo0OLD  2278  eupickbOLD  2330  2eu2ex  2340  reximi2  2801  cgsexg  2983  gencbvex  2994  vtocl3  3004  eqvinc  3064  axrep2  4380  bm1.3ii  4391  ax6vsep  4392  axnul  4395  dminss  5223  imainss  5224  iotaex  5370  fv3  5673  ssimaex  5726  dffv2  5734  exfo  5831  oprabid  6085  zfrep6  6514  frxp  6651  suppimacnvss  6669  tz7.48-1  6857  enssdom  7293  fineqvlem  7486  infcntss  7544  infeq5  7790  omex  7796  rankuni  8017  scott0  8040  acni3  8164  acnnum  8169  dfac3  8238  dfac9  8252  kmlem1  8266  cflm  8366  cfcof  8390  axdc4lem  8571  axcclem  8573  ac6c4  8597  ac6s  8600  ac6s2  8602  axdclem2  8636  brdom3  8642  brdom5  8643  brdom4  8644  axpowndlem2  8709  axpowndlem2OLD  8710  nqpr  9129  ltexprlem4  9154  reclem2pr  9163  drsdirfi  15048  2ndcsb  18757  fbssint  19115  isfil2  19133  alexsubALTlem3  19325  lpbl  19778  metustfbasOLD  19840  metustfbas  19841  3v3e3cycl2  23229  ex-natded9.26-2  23306  eqvincg  25538  19.9d2rf  25541  rexunirn  25555  ceqsexv2d  25562  cnvoprab  25703  fmcncfil  26070  0elsiga  26266  ddemeas  26361  fundmpss  27279  exisym1  27973  heiborlem3  28383  spsbce-2  29306  iotaexeu  29345  iotasbc  29346  fnchoice  29424  rfcnnnub  29431  stoweidlem35  29504  stoweidlem57  29526  hash1to3  29909  relopabVD  31215  ax6e2ndeqVD  31223  2uasbanhVD  31225  ax6e2ndeqALT  31245  bnj168  31299  bnj593  31315  bnj607  31487  bnj600  31490  bnj916  31504  bj-exa1  31678  bj-speimfw  31700  bj-axrep2  31804  bj-eumo0  31837  bj-snsetex  31903  bj-snglss  31910  bj-snglex  31913  bj-ccinftydisj  31980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597
This theorem depends on definitions:  df-bi 179  df-ex 1582
  Copyright terms: Public domain W3C validator