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

Theorem exlimdvv 1773
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 1970. (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 1772 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1772 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-ex 1658
This theorem is referenced by:  euotd  4664  funopg  5576  fmptsnd  6045  tpres  6076  opabex2  6689  fundmen  7597  undom  7613  infxpenc2  8404  zorn2lem6  8882  fpwwe2lem12  9017  genpnnp  9381  addsrmo  9448  mulsrmo  9449  hashfun  12557  hash2exprb  12580  rtrclreclem3  13067  summo  13726  fsum2dlem  13774  ntrivcvgmul  13901  prodmo  13933  fprod2dlem  13977  iscatd2  15530  gsumval3eu  17481  gsum2d2  17549  ptbasin  20534  txcls  20561  txbasval  20563  reconn  21788  phtpcer  21968  pcohtpy  21993  mbfi1flimlem  22622  mbfmullem  22625  itg2add  22659  fsumvma  24083  clwlkswlks  25428  usg2wlkonot  25553  2spontn0vne  25557  2spotdisj  25731  pconcon  29906  txscon  29916  dfpo2  30346  neibastop1  30964  itg2addnc  31903  riscer  32134  dalem62  33211  pellexlem5  35590  pellex  35592  iunrelexpuztr  36224  fzisoeu  37415  stoweidlem53  37797  stoweidlem56  37800
  Copyright terms: Public domain W3C validator