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  2332  cgsex2g  2948  cgsex4g  2949  opabss  4229  dtru  4350  copsexg  4402  elopab  4422  epelg  4455  0nelelxp  4866  elvvuni  4897  optocl  4911  xpsspw  4945  relopabi  4959  relop  4982  elreldm  5053  xpnz  5251  dfco2a  5329  unielrel  5353  unixp0  5362  oprabid  6064  1stval2  6323  2ndval2  6324  1st2val  6331  2nd2val  6332  xp1st  6335  xp2nd  6336  frxp  6415  poxp  6417  soxp  6418  rntpos  6451  dftpos4  6457  tpostpos  6458  tfrlem7  6603  th3qlem2  6970  ener  7113  domtr  7119  unen  7148  xpsnen  7151  sbthlem10  7185  mapen  7230  fseqen  7864  dfac5lem4  7963  kmlem16  8001  axdc4lem  8291  hashfacen  11658  gictr  15017  dvdsrval  15705  thlle  16879  hmphtr  17768  cusgrarn  21421  3v3e3cycl2  21604  3v3e3cycl  21605  nvss  22025  spanuni  22999  5oalem7  23115  3oalem3  23119  qqhval2  24319  wfrlem4  25473  wfrlem11  25480  frrlem4  25498  frrlem5c  25501  pprodss4v  25638  elfuns  25668  colinearex  25898  areacirc  26187  stoweidlem35  27651  bnj605  28984  bnj607  28993
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