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

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

Proof of Theorem eximi
StepHypRef Expression
1 exim 1654 . 2
2 eximi.1 . 2
31, 2mpg 1620 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1612
This theorem is referenced by:  2eximi  1657  eximii  1658  exa1  1661  exsimpl  1677  exsimpr  1678  19.29r2  1685  19.29x  1686  19.35  1687  19.40-2  1697  exlimiv  1722  speimfwOLD  1736  sbimi  1745  19.12  1950  axc9lem2  2040  exdistrf  2075  equs45f  2091  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  eumo0OLD  2317  2eu2ex  2368  reximi2  2924  cgsexg  3142  gencbvex  3153  vtocl3  3163  eqvinc  3226  axrep2  4565  bm1.3ii  4576  ax6vsep  4577  axnul  4580  copsexg  4737  dminss  5425  imainss  5426  iotaex  5573  fv3  5884  ssimaex  5938  dffv2  5946  exfo  6049  oprabid  6323  zfrep6  6768  frxp  6910  suppimacnvss  6928  tz7.48-1  7127  enssdom  7560  fineqvlem  7754  infcntss  7814  infeq5  8075  omex  8081  rankuni  8302  scott0  8325  acni3  8449  acnnum  8454  dfac3  8523  dfac9  8537  kmlem1  8551  cflm  8651  cfcof  8675  axdc4lem  8856  axcclem  8858  ac6c4  8882  ac6s  8885  ac6s2  8887  axdclem2  8921  brdom3  8927  brdom5  8928  brdom4  8929  axpowndlem2OLD  8995  nqpr  9413  ltexprlem4  9438  reclem2pr  9447  hash1to3  12530  drsdirfi  15567  2ndcsb  19950  fbssint  20339  isfil2  20357  alexsubALTlem3  20549  lpbl  21006  metustfbasOLD  21068  metustfbas  21069  3v3e3cycl2  24664  ex-natded9.26-2  25141  eqvincg  27374  19.9d2rf  27377  rexunirn  27390  fmcncfil  27913  0elsiga  28114  ddemeas  28208  fundmpss  29196  exisym1  29889  spsbce-2  31286  iotaexeu  31325  iotasbc  31326  fnchoice  31404  rfcnnnub  31411  stoweidlem35  31817  stoweidlem57  31839  relopabVD  33701  ax6e2ndeqVD  33709  2uasbanhVD  33711  ax6e2ndeqALT  33731  bnj168  33785  bnj593  33802  bnj607  33974  bnj600  33977  bnj916  33991  bj-exlime  34220  bj-nalnaleximiOLD  34222  bj-exaleximi  34224  bj-equs45fv  34331  bj-axrep2  34375  bj-eumo0  34414  bj-snsetex  34521  bj-snglss  34528  bj-snglex  34531  bj-ccinftydisj  34616  trclubg  37785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator