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

Theorem exlimdvv 1637
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 1636 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1636 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1541
This theorem is referenced by:  euotd  4349  funopg  5368  th3qlem1  6852  fundmen  7022  undom  7038  infxpenc2  7739  zorn2lem6  8218  fpwwe2lem12  8353  genpnnp  8719  hashfun  11485  summo  12287  fsum2dlem  12330  iscatd2  13682  gsumval3eu  15289  gsum2d2  15324  ptbasin  17378  txcls  17405  txbasval  17407  reconn  18436  phtpcer  18597  pcohtpy  18622  mbfi1flimlem  19181  mbfmullem  19184  itg2add  19218  fsumvma  20564  pconcon  24166  txscon  24176  rtrclreclem.trans  24447  ntrivcvgmul  24531  prodmo  24563  dfpo2  24670  itg2addnc  25494  neibastop1  25632  riscer  25942  pellexlem5  26241  pellex  26243  stoweidlem53  27125  hash2prb  27477  dalem62  29992
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-ex 1542
  Copyright terms: Public domain W3C validator