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

Theorem exlimdvv 1668
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 1664 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1664 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  euotd  4267  funopg  5286  th3qlem1  6764  fundmen  6934  undom  6950  infxpenc2  7649  zorn2lem6  8128  fpwwe2lem12  8263  genpnnp  8629  hashfun  11389  summo  12190  fsum2dlem  12233  iscatd2  13583  gsumval3eu  15190  gsum2d2  15225  ptbasin  17272  txcls  17299  txbasval  17301  reconn  18333  phtpcer  18493  pcohtpy  18518  mbfi1flimlem  19077  mbfmullem  19080  itg2add  19114  fsumvma  20452  pconcon  23762  txscon  23772  rtrclreclem.trans  24043  dfpo2  24112  neibastop1  26308  riscer  26619  pellexlem5  26918  pellex  26920  stoweidlem53  27802  dalem62  29923
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator