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

Theorem exlimivv 2026
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 2024 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 2024 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537
This theorem is referenced by:  2mo  2194  cgsex2g  2788  cgsex4g  2789  opabss  4040  dtru  4159  copsexg  4210  elopab  4230  epelg  4264  0nelelxp  4692  elvvuni  4724  optocl  4738  xpsspw  4771  relopabi  4785  relop  4808  elreldm  4877  xpnz  5073  dfco2a  5146  unielrel  5170  unixp0  5179  oprabid  5802  1stval2  6057  2ndval2  6058  1st2val  6065  2nd2val  6066  xp1st  6069  xp2nd  6070  frxp  6145  poxp  6147  soxp  6148  rntpos  6167  dftpos4  6173  tpostpos  6174  tfrlem7  6353  th3qlem2  6719  ener  6862  domtr  6868  unen  6897  xpsnen  6900  sbthlem10  6934  mapen  6979  fseqen  7608  dfac5lem4  7707  kmlem16  7745  axdc4lem  8035  hashfacen  11343  gictr  14687  dvdsrval  15375  thlle  16545  hmphtr  17422  nvss  21095  spanuni  22069  5oalem7  22203  3oalem3  22207  wfrlem4  23614  wfrlem11  23621  frrlem4  23639  frrlem5c  23642  pprodss4v  23786  elfuns  23815  colinearex  24044  copsexgb  24318  stcat  24396  eloi  24438  cbcpcp  24515  cmpmor  25328  stoweidlem35  27105  bnj605  27972  bnj607  27981
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator