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

Theorem exlimivv 2025
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 2023 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 2023 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  2191  cgsex2g  2758  cgsex4g  2759  opabss  3977  dtru  4095  copsexg  4145  elopab  4165  epelg  4199  0nelelxp  4625  elvvuni  4657  optocl  4671  xpsspw  4704  relopabi  4718  relop  4741  elreldm  4810  xpnz  5006  dfco2a  5079  unielrel  5103  unixp0  5112  oprabid  5734  1stval2  5989  2ndval2  5990  1st2val  5997  2nd2val  5998  xp1st  6001  xp2nd  6002  frxp  6077  poxp  6079  soxp  6080  rntpos  6099  dftpos4  6105  tpostpos  6106  tfrlem7  6285  th3qlem2  6651  ener  6794  domtr  6799  unen  6828  xpsnen  6831  sbthlem10  6865  mapen  6910  fseqen  7538  dfac5lem4  7637  kmlem16  7675  axdc4lem  7965  hashfacen  11269  gictr  14574  dvdsrval  15262  thlle  16429  hmphtr  17306  nvss  20979  spanuni  21953  5oalem7  22087  3oalem3  22091  wfrlem4  23427  wfrlem11  23434  frrlem4  23452  frrlem5c  23455  pprodss4v  23599  elfuns  23628  colinearex  23857  copsexgb  24131  stcat  24209  eloi  24251  cbcpcp  24328  cmpmor  25141  bnj605  27628  bnj607  27637
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