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

Theorem exlimivv 1642
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 1641 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1641 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1547
This theorem is referenced by:  2mo  2336  cgsex2g  2952  cgsex4g  2953  opabss  4233  dtru  4354  copsexg  4406  elopab  4426  epelg  4459  0nelelxp  4870  elvvuni  4901  optocl  4915  xpsspw  4949  relopabi  4963  relop  4986  elreldm  5057  xpnz  5255  dfco2a  5333  unielrel  5357  unixp0  5366  oprabid  6068  1stval2  6327  2ndval2  6328  1st2val  6335  2nd2val  6336  xp1st  6339  xp2nd  6340  frxp  6419  poxp  6421  soxp  6422  rntpos  6455  dftpos4  6461  tpostpos  6462  tfrlem7  6607  th3qlem2  6974  ener  7117  domtr  7123  unen  7152  xpsnen  7155  sbthlem10  7189  mapen  7234  fseqen  7868  dfac5lem4  7967  kmlem16  8005  axdc4lem  8295  hashfacen  11662  gictr  15021  dvdsrval  15709  thlle  16883  hmphtr  17772  cusgrarn  21425  3v3e3cycl2  21608  3v3e3cycl  21609  nvss  22029  spanuni  23003  5oalem7  23119  3oalem3  23123  qqhval2  24323  wfrlem4  25477  wfrlem11  25484  frrlem4  25502  frrlem5c  25505  pprodss4v  25642  elfuns  25672  colinearex  25902  areacirc  26191  stoweidlem35  27655  bnj605  28988  bnj607  28997
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator