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

Theorem exlimivv 1635
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 1634 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1634 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1541
This theorem is referenced by:  2mo  2287  cgsex2g  2896  cgsex4g  2897  opabss  4161  dtru  4282  copsexg  4334  elopab  4354  epelg  4388  0nelelxp  4800  elvvuni  4832  optocl  4846  xpsspw  4879  relopabi  4893  relop  4916  elreldm  4985  xpnz  5181  dfco2a  5255  unielrel  5279  unixp0  5288  oprabid  5969  1stval2  6224  2ndval2  6225  1st2val  6232  2nd2val  6233  xp1st  6236  xp2nd  6237  frxp  6312  poxp  6314  soxp  6315  rntpos  6334  dftpos4  6340  tpostpos  6341  tfrlem7  6486  th3qlem2  6853  ener  6996  domtr  7002  unen  7031  xpsnen  7034  sbthlem10  7068  mapen  7113  fseqen  7744  dfac5lem4  7843  kmlem16  7881  axdc4lem  8171  hashfacen  11488  gictr  14838  dvdsrval  15526  thlle  16703  hmphtr  17580  nvss  21263  spanuni  22237  5oalem7  22353  3oalem3  22357  qqhval2  23639  wfrlem4  24817  wfrlem11  24824  frrlem4  24842  frrlem5c  24845  pprodss4v  24982  elfuns  25012  colinearex  25242  areacirc  25523  stoweidlem35  27107  cusgrarn  27622  3v3e3cycl2  27788  3v3e3cycl  27789  bnj605  28701  bnj607  28710
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-ex 1542
  Copyright terms: Public domain W3C validator