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

Theorem exlimdvv 1691
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 1690 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1690 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670
This theorem depends on definitions:  df-bi 185  df-ex 1587
This theorem is referenced by:  euotd  4613  funopg  5471  opabex2  6537  th3qlem1  7227  fundmen  7404  undom  7420  infxpenc2  8209  infxpenc2OLD  8213  zorn2lem6  8691  fpwwe2lem12  8829  genpnnp  9195  hash2prb  12201  hashfun  12220  summo  13215  fsum2dlem  13258  iscatd2  14640  gsumval3eu  16402  gsum2d2  16488  ptbasin  19172  txcls  19199  txbasval  19201  reconn  20427  phtpcer  20589  pcohtpy  20614  mbfi1flimlem  21222  mbfmullem  21225  itg2add  21259  fsumvma  22574  pconcon  27142  txscon  27152  rtrclreclem.trans  27370  ntrivcvgmul  27439  prodmo  27471  fprod2dlem  27513  dfpo2  27587  itg2addnc  28472  neibastop1  28606  riscer  28820  pellexlem5  29200  pellex  29202  stoweidlem53  29874  stoweidlem56  29877  usg2wlkonot  30428  2spontn0vne  30432  clwlkswlks  30449  2spotdisj  30680  fmptsnd  30748  dalem62  33474
  Copyright terms: Public domain W3C validator