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

Theorem exlimivv 2012
 Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2236. (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 2010 . 2 (∃𝑦𝜑𝜓)
32exlimiv 2010 1 (∃𝑥𝑦𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1852 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991 This theorem depends on definitions:  df-bi 197  df-ex 1853 This theorem is referenced by:  cgsex2g  3391  cgsex4g  3392  opabss  4848  dtru  4988  copsexg  5083  elopab  5116  elopabr  5146  epelg  5163  0nelelxp  5285  elvvuni  5319  optocl  5335  relopabiALT  5385  relop  5411  elreldm  5488  xpnz  5694  xpdifid  5703  dfco2a  5779  unielrel  5804  unixp0  5813  funsndifnop  6559  fmptsng  6578  oprabid  6822  oprabv  6850  1stval2  7332  2ndval2  7333  1st2val  7343  2nd2val  7344  xp1st  7347  xp2nd  7348  frxp  7438  poxp  7440  soxp  7441  rntpos  7517  dftpos4  7523  tpostpos  7524  wfrlem4  7570  wfrlem4OLD  7571  wfrfun  7578  tfrlem7  7632  ener  8156  domtr  8162  unen  8196  xpsnen  8200  sbthlem10  8235  mapen  8280  djuunxp  8947  fseqen  9050  dfac5lem4  9149  kmlem16  9189  axdc4lem  9479  hashfacen  13440  hashle2pr  13461  fundmge2nop0  13476  gictr  17925  dvdsrval  18853  thlle  20258  hmphtr  21807  griedg0ssusgr  26380  rgrusgrprc  26720  numclwwlk1lem2fo  27544  frgrregord013  27594  friendship  27598  nvss  27788  spanuni  28743  5oalem7  28859  3oalem3  28863  opabssi  29763  gsummpt2co  30120  qqhval2  30366  bnj605  31315  bnj607  31324  mppspstlem  31806  mppsval  31807  frrlem4  32120  frrlem5c  32123  pprodss4v  32328  sscoid  32357  colinearex  32504  bj-dtru  33133  cnfinltrel  33578  stoweidlem35  40769  funop1  41825  sprsymrelfvlem  42268  uspgrsprf  42282  uspgrsprf1  42283
 Copyright terms: Public domain W3C validator