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

Theorem exlimdvv 2026
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
exlimdvv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
exlimdvv  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Distinct variable groups:    ch, x    ph, x    ch, y    ph, y
Allowed substitution hints:    ps( x, y)

Proof of Theorem exlimdvv
StepHypRef Expression
1 exlimdvv.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21exlimdv 1932 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1932 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537
This theorem is referenced by:  euotd  4160  funopg  5144  th3qlem1  6650  fundmen  6819  undom  6835  infxpenc2  7533  zorn2lem6  8012  fpwwe2lem12  8143  genpnnp  8509  hashfun  11266  summo  12067  fsum2dlem  12110  iscatd2  13427  gsumval3eu  15025  gsum2d2  15060  ptbasin  17104  txcls  17131  txbasval  17133  reconn  18165  phtpcer  18325  pcohtpy  18350  mbfi1flimlem  18909  mbfmullem  18912  itg2add  18946  fsumvma  20284  pconcon  22933  txscon  22943  rtrclreclem.trans  23214  dfpo2  23282  neibastop1  25474  riscer  25785  pellexlem5  26084  pellex  26086  dalem62  28612
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