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

Theorem exlimdvv 1934
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2211. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
exlimdvv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
exlimdvv (𝜑 → (∃𝑥𝑦𝜓𝜒))
Distinct variable groups:   𝜒,𝑥   𝜑,𝑥   𝜒,𝑦   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem exlimdvv
StepHypRef Expression
1 exlimdvv.1 . . 3 (𝜑 → (𝜓𝜒))
21exlimdv 1933 . 2 (𝜑 → (∃𝑦𝜓𝜒))
32exlimdv 1933 1 (𝜑 → (∃𝑥𝑦𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  euotd  5518  opabssxpd  5732  dfpo2  6316  funopg  6600  fmptsnd  7189  tpres  7221  opreuopreu  8059  frxp2  8169  frxp3  8176  fundmen  9071  undomOLD  9100  ttrcltr  9756  infxpenc2  10062  zorn2lem6  10541  fpwwe2lem11  10681  genpnnp  11045  addsrmo  11113  mulsrmo  11114  hashfun  14476  hash2exprb  14510  hash3tpexb  14533  rtrclreclem3  15099  summo  15753  fsum2dlem  15806  ntrivcvgmul  15938  prodmo  15972  fprod2dlem  16016  iscatd2  17724  gsumval3eu  19922  gsum2d2  19992  ptbasin  23585  txcls  23612  txbasval  23614  reconn  24850  phtpcer  25027  pcohtpy  25053  mbfi1flimlem  25757  mbfmullem  25760  itg2add  25794  fsumvma  27257  umgr3v3e3cycl  30203  conngrv2edg  30214  brab2d  32619  2ndresdju  32659  cusgracyclt3v  35161  pconnconn  35236  txsconn  35246  neibastop1  36360  itg2addnc  37681  riscer  37995  dalem62  39736  pellexlem5  42844  pellex  42846  nnoeomeqom  43325  iunrelexpuztr  43732  fzisoeu  45312  stoweidlem53  46068  stoweidlem56  46071  fundcmpsurinjpreimafv  47395  ichnreuop  47459  brab2dd  48741
  Copyright terms: Public domain W3C validator