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

Theorem exlimdvv 1690
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 1689 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1689 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669
This theorem depends on definitions:  df-bi 185  df-ex 1590
This theorem is referenced by:  euotd  4580  funopg  5438  opabex2  6505  th3qlem1  7194  fundmen  7371  undom  7387  infxpenc2  8176  infxpenc2OLD  8180  zorn2lem6  8658  fpwwe2lem12  8795  genpnnp  9161  hash2prb  12163  hashfun  12182  summo  13177  fsum2dlem  13220  iscatd2  14601  gsumval3eu  16360  gsum2d2  16439  ptbasin  18991  txcls  19018  txbasval  19020  reconn  20246  phtpcer  20408  pcohtpy  20433  mbfi1flimlem  21041  mbfmullem  21044  itg2add  21078  fsumvma  22436  pconcon  26967  txscon  26977  rtrclreclem.trans  27194  ntrivcvgmul  27263  prodmo  27295  fprod2dlem  27337  dfpo2  27411  itg2addnc  28287  neibastop1  28421  riscer  28635  pellexlem5  29016  pellex  29018  stoweidlem53  29691  stoweidlem56  29694  usg2wlkonot  30245  2spontn0vne  30249  clwlkswlks  30266  2spotdisj  30497  fmptsnd  30564  dalem62  32948
  Copyright terms: Public domain W3C validator