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

Theorem exlimivv 1668
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 1667 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1667 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  2222  cgsex2g  2821  cgsex4g  2822  opabss  4081  dtru  4200  copsexg  4251  elopab  4271  epelg  4305  0nelelxp  4717  elvvuni  4749  optocl  4763  xpsspw  4796  relopabi  4810  relop  4833  elreldm  4902  xpnz  5098  dfco2a  5171  unielrel  5195  unixp0  5204  oprabid  5844  1stval2  6099  2ndval2  6100  1st2val  6107  2nd2val  6108  xp1st  6111  xp2nd  6112  frxp  6187  poxp  6189  soxp  6190  rntpos  6209  dftpos4  6215  tpostpos  6216  tfrlem7  6395  th3qlem2  6761  ener  6904  domtr  6910  unen  6939  xpsnen  6942  sbthlem10  6976  mapen  7021  fseqen  7650  dfac5lem4  7749  kmlem16  7787  axdc4lem  8077  hashfacen  11388  gictr  14735  dvdsrval  15423  thlle  16593  hmphtr  17470  nvss  21143  spanuni  22119  5oalem7  22235  3oalem3  22239  wfrlem4  23663  wfrlem11  23670  frrlem4  23688  frrlem5c  23691  pprodss4v  23835  elfuns  23864  colinearex  24093  areacirc  24341  copsexgb  24376  stcat  24454  eloi  24496  cbcpcp  24573  cmpmor  25386  stoweidlem35  27195  bnj605  28218  bnj607  28227
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 1636  ax-8 1644
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator