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

Theorem exlimivv 1625
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 1624 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1624 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1531
This theorem is referenced by:  2mo  2234  cgsex2g  2833  cgsex4g  2834  opabss  4096  dtru  4217  copsexg  4268  elopab  4288  epelg  4322  0nelelxp  4734  elvvuni  4766  optocl  4780  xpsspw  4813  relopabi  4827  relop  4850  elreldm  4919  xpnz  5115  dfco2a  5189  unielrel  5213  unixp0  5222  oprabid  5898  1stval2  6153  2ndval2  6154  1st2val  6161  2nd2val  6162  xp1st  6165  xp2nd  6166  frxp  6241  poxp  6243  soxp  6244  rntpos  6263  dftpos4  6269  tpostpos  6270  tfrlem7  6415  th3qlem2  6781  ener  6924  domtr  6930  unen  6959  xpsnen  6962  sbthlem10  6996  mapen  7041  fseqen  7670  dfac5lem4  7769  kmlem16  7807  axdc4lem  8097  hashfacen  11408  gictr  14755  dvdsrval  15443  thlle  16613  hmphtr  17490  nvss  21165  spanuni  22139  5oalem7  22255  3oalem3  22259  wfrlem4  24330  wfrlem11  24337  frrlem4  24355  frrlem5c  24358  pprodss4v  24495  elfuns  24525  colinearex  24755  areacirc  25034  copsexgb  25069  stcat  25147  eloi  25189  cbcpcp  25265  cmpmor  26078  stoweidlem35  27887  3v3e3cycl2  28410  3v3e3cycl  28411  bnj605  29255  bnj607  29264
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator