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

Theorem exlimdvv 1710
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 1894. (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 1709 . 2  |-  ( ph  ->  ( E. y ps 
->  ch ) )
32exlimdv 1709 1  |-  ( ph  ->  ( E. x E. y ps  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689
This theorem depends on definitions:  df-bi 185  df-ex 1598
This theorem is referenced by:  euotd  4735  funopg  5607  fmptsnd  6075  opabex2  6720  fundmen  7588  undom  7604  infxpenc2  8399  infxpenc2OLD  8403  zorn2lem6  8881  fpwwe2lem12  9019  genpnnp  9383  addsrmo  9450  mulsrmo  9451  hashfun  12471  hash2prb  12493  summo  13515  fsum2dlem  13561  iscatd2  14952  gsumval3eu  16778  gsum2d2  16873  ptbasin  19948  txcls  19975  txbasval  19977  reconn  21203  phtpcer  21365  pcohtpy  21390  mbfi1flimlem  21999  mbfmullem  22002  itg2add  22036  fsumvma  23357  clwlkswlks  24627  usg2wlkonot  24752  2spontn0vne  24756  2spotdisj  24930  pconcon  28546  txscon  28556  rtrclreclem.trans  28939  ntrivcvgmul  29008  prodmo  29040  fprod2dlem  29082  dfpo2  29156  itg2addnc  30041  neibastop1  30149  riscer  30363  pellexlem5  30741  pellex  30743  fzisoeu  31449  stoweidlem53  31724  stoweidlem56  31727  tpres  32390  dalem62  35181
  Copyright terms: Public domain W3C validator