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  2196  cgsex2g  2795  cgsex4g  2796  opabss  4054  dtru  4173  copsexg  4224  elopab  4244  epelg  4278  0nelelxp  4706  elvvuni  4738  optocl  4752  xpsspw  4785  relopabi  4799  relop  4822  elreldm  4891  xpnz  5087  dfco2a  5160  unielrel  5184  unixp0  5193  oprabid  5816  1stval2  6071  2ndval2  6072  1st2val  6079  2nd2val  6080  xp1st  6083  xp2nd  6084  frxp  6159  poxp  6161  soxp  6162  rntpos  6181  dftpos4  6187  tpostpos  6188  tfrlem7  6367  th3qlem2  6733  ener  6876  domtr  6882  unen  6911  xpsnen  6914  sbthlem10  6948  mapen  6993  fseqen  7622  dfac5lem4  7721  kmlem16  7759  axdc4lem  8049  hashfacen  11358  gictr  14702  dvdsrval  15390  thlle  16560  hmphtr  17437  nvss  21110  spanuni  22084  5oalem7  22200  3oalem3  22204  wfrlem4  23629  wfrlem11  23636  frrlem4  23654  frrlem5c  23657  pprodss4v  23801  elfuns  23830  colinearex  24059  copsexgb  24333  stcat  24411  eloi  24453  cbcpcp  24530  cmpmor  25343  stoweidlem35  27153  bnj605  28071  bnj607  28080
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