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

Theorem exlimivv 1669
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)
Hypothesis
Ref Expression
exlimivv.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
exlimivv  |-  ( E. x E. y ph  ->  ps )
Distinct variable groups:    ps, x    ps, y
Allowed substitution hints:    ph( x, y)

Proof of Theorem exlimivv
StepHypRef Expression
1 exlimivv.1 . . 3  |-  ( ph  ->  ps )
21exlimiv 1668 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1668 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1530
This theorem is referenced by:  2mo  2223  cgsex2g  2822  cgsex4g  2823  opabss  4082  dtru  4203  copsexg  4254  elopab  4274  epelg  4308  0nelelxp  4720  elvvuni  4752  optocl  4766  xpsspw  4799  relopabi  4813  relop  4836  elreldm  4905  xpnz  5101  dfco2a  5175  unielrel  5199  unixp0  5208  oprabid  5884  1stval2  6139  2ndval2  6140  1st2val  6147  2nd2val  6148  xp1st  6151  xp2nd  6152  frxp  6227  poxp  6229  soxp  6230  rntpos  6249  dftpos4  6255  tpostpos  6256  tfrlem7  6401  th3qlem2  6767  ener  6910  domtr  6916  unen  6945  xpsnen  6948  sbthlem10  6982  mapen  7027  fseqen  7656  dfac5lem4  7755  kmlem16  7793  axdc4lem  8083  hashfacen  11394  gictr  14741  dvdsrval  15429  thlle  16599  hmphtr  17476  nvss  21151  spanuni  22125  5oalem7  22241  3oalem3  22245  wfrlem4  24261  wfrlem11  24268  frrlem4  24286  frrlem5c  24289  pprodss4v  24426  elfuns  24456  colinearex  24685  areacirc  24942  copsexgb  24977  stcat  25055  eloi  25097  cbcpcp  25173  cmpmor  25986  stoweidlem35  27795  bnj605  29012  bnj607  29021
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1531
  Copyright terms: Public domain W3C validator