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

Theorem exlimdvv 2027
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 1933 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1933 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537
This theorem is referenced by:  euotd  4204  funopg  5190  th3qlem1  6697  fundmen  6867  undom  6883  infxpenc2  7582  zorn2lem6  8061  fpwwe2lem12  8196  genpnnp  8562  hashfun  11319  summo  12120  fsum2dlem  12163  iscatd2  13510  gsumval3eu  15117  gsum2d2  15152  ptbasin  17199  txcls  17226  txbasval  17228  reconn  18260  phtpcer  18420  pcohtpy  18445  mbfi1flimlem  19004  mbfmullem  19007  itg2add  19041  fsumvma  20379  pconcon  23099  txscon  23109  rtrclreclem.trans  23380  dfpo2  23448  neibastop1  25640  riscer  25951  pellexlem5  26250  pellex  26252  stoweidlem53  27102  dalem62  29053
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator