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

Theorem exlimdvv 2029
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2244. (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 2028 . 2 (𝜑 → (∃𝑦𝜓𝜒))
32exlimdv 2028 1 (𝜑 → (∃𝑥𝑦𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-ex 1875
This theorem is referenced by:  euotd  5136  opabssxpd  5508  funopg  6104  fmptsnd  6630  tpres  6661  fundmen  8236  undom  8257  infxpenc2  9098  zorn2lem6  9578  fpwwe2lem12  9718  genpnnp  10082  addsrmo  10149  mulsrmo  10150  hashfun  13428  hash2exprb  13457  rtrclreclem3  14088  summo  14736  fsum2dlem  14789  ntrivcvgmul  14920  prodmo  14952  fprod2dlem  14996  iscatd2  16610  gsumval3eu  18574  gsum2d2  18642  ptbasin  21663  txcls  21690  txbasval  21692  reconn  22913  phtpcer  23076  pcohtpy  23101  mbfi1flimlem  23783  mbfmullem  23786  itg2add  23820  fsumvma  25232  umgr3v3e3cycl  27465  conngrv2edg  27476  pconnconn  31664  txsconn  31674  dfpo2  32093  neibastop1  32800  itg2addnc  33890  riscer  34212  dalem62  35693  pellexlem5  38078  pellex  38080  iunrelexpuztr  38689  fzisoeu  40156  stoweidlem53  40910  stoweidlem56  40913
  Copyright terms: Public domain W3C validator