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

Theorem exlimivv 1645
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 1644 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1644 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550
This theorem is referenced by:  2mo  2359  cgsex2g  2988  cgsex4g  2989  opabss  4269  dtru  4390  copsexg  4442  elopab  4462  epelg  4495  0nelelxp  4907  elvvuni  4938  optocl  4952  xpsspw  4986  relopabi  5000  relop  5023  elreldm  5094  xpnz  5292  dfco2a  5370  unielrel  5394  unixp0  5403  oprabid  6105  1stval2  6364  2ndval2  6365  1st2val  6372  2nd2val  6373  xp1st  6376  xp2nd  6377  frxp  6456  poxp  6458  soxp  6459  rntpos  6492  dftpos4  6498  tpostpos  6499  tfrlem7  6644  th3qlem2  7011  ener  7154  domtr  7160  unen  7189  xpsnen  7192  sbthlem10  7226  mapen  7271  fseqen  7908  dfac5lem4  8007  kmlem16  8045  axdc4lem  8335  hashfacen  11703  gictr  15062  dvdsrval  15750  thlle  16924  hmphtr  17815  cusgrarn  21468  3v3e3cycl2  21651  3v3e3cycl  21652  nvss  22072  spanuni  23046  5oalem7  23162  3oalem3  23166  qqhval2  24366  wfrlem4  25541  wfrlem11  25548  frrlem4  25585  frrlem5c  25588  pprodss4v  25729  sscoid  25758  colinearex  25994  areacirc  26297  stoweidlem35  27760  oprabv  28085  bnj605  29278  bnj607  29287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator