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

Theorem exlimivv 1667
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 1666 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1666 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  2mo  2221  cgsex2g  2820  cgsex4g  2821  opabss  4080  dtru  4201  copsexg  4252  elopab  4272  epelg  4306  0nelelxp  4718  elvvuni  4750  optocl  4764  xpsspw  4797  relopabi  4811  relop  4834  elreldm  4903  xpnz  5099  dfco2a  5173  unielrel  5197  unixp0  5206  oprabid  5882  1stval2  6137  2ndval2  6138  1st2val  6145  2nd2val  6146  xp1st  6149  xp2nd  6150  frxp  6225  poxp  6227  soxp  6228  rntpos  6247  dftpos4  6253  tpostpos  6254  tfrlem7  6399  th3qlem2  6765  ener  6908  domtr  6914  unen  6943  xpsnen  6946  sbthlem10  6980  mapen  7025  fseqen  7654  dfac5lem4  7753  kmlem16  7791  axdc4lem  8081  hashfacen  11392  gictr  14739  dvdsrval  15427  thlle  16597  hmphtr  17474  nvss  21149  spanuni  22123  5oalem7  22239  3oalem3  22243  wfrlem4  23670  wfrlem11  23677  frrlem4  23695  frrlem5c  23698  pprodss4v  23835  elfuns  23865  colinearex  24094  areacirc  24343  copsexgb  24378  stcat  24456  eloi  24498  cbcpcp  24574  cmpmor  25387  stoweidlem35  27196  bnj605  28312  bnj607  28321
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator