MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exlimivv Structured version   Visualization version   GIF version

Theorem exlimivv 1846
Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2066. (Contributed by NM, 1-Aug-1995.)
Hypothesis
Ref Expression
exlimivv.1 (𝜑𝜓)
Assertion
Ref Expression
exlimivv (∃𝑥𝑦𝜑𝜓)
Distinct variable groups:   𝜓,𝑥   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem exlimivv
StepHypRef Expression
1 exlimivv.1 . . 3 (𝜑𝜓)
21exlimiv 1844 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1844 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  cgsex2g  3211  cgsex4g  3212  opabss  4640  dtru  4778  copsexg  4876  elopab  4898  elopabr  4927  epelg  4940  0nelelxp  5059  elvvuni  5092  optocl  5108  relopabi  5156  relop  5182  elreldm  5258  xpnz  5458  xpdifid  5467  dfco2a  5538  unielrel  5563  unixp0  5572  fmptsng  6317  oprabid  6554  oprabv  6579  1stval2  7053  2ndval2  7054  1st2val  7062  2nd2val  7063  xp1st  7066  xp2nd  7067  frxp  7151  poxp  7153  soxp  7154  rntpos  7229  dftpos4  7235  tpostpos  7236  wfrlem4  7282  wfrfun  7289  tfrlem7  7343  ener  7865  enerOLD  7866  domtr  7872  unen  7902  xpsnen  7906  sbthlem10  7941  mapen  7986  fseqen  8710  dfac5lem4  8809  kmlem16  8847  axdc4lem  9137  hashfacen  13047  gictr  17486  dvdsrval  18414  thlle  19802  hmphtr  21338  usgrac  25646  edgss  25647  cusgrarn  25754  3v3e3cycl2  25958  3v3e3cycl  25959  numclwlk1lem2fo  26388  frgraregord013  26411  friendship  26415  nvss  26616  spanuni  27593  5oalem7  27709  3oalem3  27713  gsummpt2co  28917  qqhval2  29160  bnj605  30037  bnj607  30046  mppspstlem  30528  mppsval  30529  frrlem4  30833  frrlem5c  30836  pprodss4v  30967  sscoid  30996  colinearex  31143  bj-dtru  31791  stoweidlem35  38725  funop1  40139  funsndifnop  40141  fundmge2nop0  40145  griedg0ssusgr  40484  rgrusgrprc  40784  av-numclwlk1lem2fo  41520  av-frgraregord013  41544  av-friendship  41548
  Copyright terms: Public domain W3C validator