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

Theorem exlimdvv 2027
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 1933 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1933 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  4239  funopg  5225  th3qlem1  6732  fundmen  6902  undom  6918  infxpenc2  7617  zorn2lem6  8096  fpwwe2lem12  8231  genpnnp  8597  hashfun  11354  summo  12155  fsum2dlem  12198  iscatd2  13545  gsumval3eu  15152  gsum2d2  15187  ptbasin  17234  txcls  17261  txbasval  17263  reconn  18295  phtpcer  18455  pcohtpy  18480  mbfi1flimlem  19039  mbfmullem  19042  itg2add  19076  fsumvma  20414  pconcon  23134  txscon  23144  rtrclreclem.trans  23415  dfpo2  23483  neibastop1  25675  riscer  25986  pellexlem5  26285  pellex  26287  stoweidlem53  27137  dalem62  29090
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