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

Theorem exlimdvv 1701
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 1700 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1700 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  euotd  4754  funopg  5626  fmptsnd  6094  opabex2  6733  fundmen  7601  undom  7617  infxpenc2  8411  infxpenc2OLD  8415  zorn2lem6  8893  fpwwe2lem12  9031  genpnnp  9395  addsrmo  9462  mulsrmo  9463  hashfun  12476  hash2prb  12498  summo  13519  fsum2dlem  13565  iscatd2  14953  gsumval3eu  16780  gsum2d2  16875  ptbasin  19946  txcls  19973  txbasval  19975  reconn  21201  phtpcer  21363  pcohtpy  21388  mbfi1flimlem  21997  mbfmullem  22000  itg2add  22034  fsumvma  23354  clwlkswlks  24581  usg2wlkonot  24706  2spontn0vne  24710  2spotdisj  24885  pconcon  28501  txscon  28511  rtrclreclem.trans  28894  ntrivcvgmul  28963  prodmo  28995  fprod2dlem  29037  dfpo2  29111  itg2addnc  29996  neibastop1  30104  riscer  30318  pellexlem5  30697  pellex  30699  fzisoeu  31400  stoweidlem53  31676  stoweidlem56  31679  dalem62  34931
  Copyright terms: Public domain W3C validator