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

Theorem exlimdvv 1860
 Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2078. (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 1859 . 2 (𝜑 → (∃𝑦𝜓𝜒))
32exlimdv 1859 1 (𝜑 → (∃𝑥𝑦𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1702 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837 This theorem depends on definitions:  df-bi 197  df-ex 1703 This theorem is referenced by:  euotd  4965  opabssxpd  5327  funopg  5910  fmptsnd  6420  tpres  6451  fundmen  8015  undom  8033  infxpenc2  8830  zorn2lem6  9308  fpwwe2lem12  9448  genpnnp  9812  addsrmo  9879  mulsrmo  9880  hashfun  13207  hash2exprb  13236  rtrclreclem3  13781  summo  14429  fsum2dlem  14482  ntrivcvgmul  14615  prodmo  14647  fprod2dlem  14691  iscatd2  16323  gsumval3eu  18286  gsum2d2  18354  ptbasin  21361  txcls  21388  txbasval  21390  reconn  22612  phtpcer  22775  phtpcerOLD  22776  pcohtpy  22801  mbfi1flimlem  23470  mbfmullem  23473  itg2add  23507  fsumvma  24919  umgr3v3e3cycl  27024  conngrv2edg  27035  pconnconn  31187  txsconn  31197  dfpo2  31620  neibastop1  32329  itg2addnc  33435  riscer  33758  dalem62  34839  pellexlem5  37216  pellex  37218  iunrelexpuztr  37830  fzisoeu  39327  stoweidlem53  40033  stoweidlem56  40036
 Copyright terms: Public domain W3C validator