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

Theorem exlimdvv 1669
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 1665 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1665 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1529
This theorem is referenced by:  euotd  4267  funopg  5253  th3qlem1  6760  fundmen  6930  undom  6946  infxpenc2  7645  zorn2lem6  8124  fpwwe2lem12  8259  genpnnp  8625  hashfun  11384  summo  12185  fsum2dlem  12228  iscatd2  13578  gsumval3eu  15185  gsum2d2  15220  ptbasin  17267  txcls  17294  txbasval  17296  reconn  18328  phtpcer  18488  pcohtpy  18513  mbfi1flimlem  19072  mbfmullem  19075  itg2add  19109  fsumvma  20447  pconcon  23167  txscon  23177  rtrclreclem.trans  23448  dfpo2  23516  neibastop1  25708  riscer  26019  pellexlem5  26318  pellex  26320  stoweidlem53  27202  dalem62  29191
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530
  Copyright terms: Public domain W3C validator