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

Theorem exlimdvv 1649
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 1648 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1648 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1551
This theorem is referenced by:  euotd  4492  funopg  5520  th3qlem1  7046  fundmen  7216  undom  7232  infxpenc2  7941  zorn2lem6  8419  fpwwe2lem12  8554  genpnnp  8920  hash2prb  11727  hashfun  11738  summo  12549  fsum2dlem  12592  iscatd2  13944  gsumval3eu  15551  gsum2d2  15586  ptbasin  17647  txcls  17674  txbasval  17676  reconn  18897  phtpcer  19058  pcohtpy  19083  mbfi1flimlem  19650  mbfmullem  19653  itg2add  19687  fsumvma  21035  pconcon  24953  txscon  24963  rtrclreclem.trans  25181  ntrivcvgmul  25265  prodmo  25297  fprod2dlem  25339  dfpo2  25413  itg2addnc  26301  neibastop1  26430  riscer  26646  pellexlem5  27008  pellex  27010  stoweidlem53  27890  stoweidlem56  27893  usg2wlkonot  28513  2spontn0vne  28517  2spotdisj  28622  dalem62  30705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator