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  2771  cgsex4g  2772  opabss  4020  dtru  4139  copsexg  4189  elopab  4209  epelg  4243  0nelelxp  4671  elvvuni  4703  optocl  4717  xpsspw  4750  relopabi  4764  relop  4787  elreldm  4856  xpnz  5052  dfco2a  5125  unielrel  5149  unixp0  5158  oprabid  5781  1stval2  6036  2ndval2  6037  1st2val  6044  2nd2val  6045  xp1st  6048  xp2nd  6049  frxp  6124  poxp  6126  soxp  6127  rntpos  6146  dftpos4  6152  tpostpos  6153  tfrlem7  6332  th3qlem2  6698  ener  6841  domtr  6847  unen  6876  xpsnen  6879  sbthlem10  6913  mapen  6958  fseqen  7587  dfac5lem4  7686  kmlem16  7724  axdc4lem  8014  hashfacen  11322  gictr  14666  dvdsrval  15354  thlle  16524  hmphtr  17401  nvss  21074  spanuni  22048  5oalem7  22182  3oalem3  22186  wfrlem4  23593  wfrlem11  23600  frrlem4  23618  frrlem5c  23621  pprodss4v  23765  elfuns  23794  colinearex  24023  copsexgb  24297  stcat  24375  eloi  24417  cbcpcp  24494  cmpmor  25307  stoweidlem35  27084  bnj605  27951  bnj607  27960
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