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

Theorem exlimdvv 1644
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 1643 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1643 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1547
This theorem is referenced by:  euotd  4425  funopg  5452  th3qlem1  6977  fundmen  7147  undom  7163  infxpenc2  7867  zorn2lem6  8345  fpwwe2lem12  8480  genpnnp  8846  hash2prb  11652  hashfun  11663  summo  12474  fsum2dlem  12517  iscatd2  13869  gsumval3eu  15476  gsum2d2  15511  ptbasin  17570  txcls  17597  txbasval  17599  reconn  18820  phtpcer  18981  pcohtpy  19006  mbfi1flimlem  19575  mbfmullem  19578  itg2add  19612  fsumvma  20958  pconcon  24879  txscon  24889  rtrclreclem.trans  25107  ntrivcvgmul  25191  prodmo  25223  fprod2dlem  25265  dfpo2  25334  itg2addnc  26166  neibastop1  26286  riscer  26502  pellexlem5  26794  pellex  26796  stoweidlem53  27677  stoweidlem56  27680  usg2wlkonot  28088  2spontn0vne  28092  2spotdisj  28172  dalem62  30228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator