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

Theorem exlimdvv 1847
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2064. (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 1846 . 2 (𝜑 → (∃𝑦𝜓𝜒))
32exlimdv 1846 1 (𝜑 → (∃𝑥𝑦𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  euotd  4887  funopg  5818  fmptsnd  6314  tpres  6345  opabex2  6970  fundmen  7889  undom  7906  infxpenc2  8701  zorn2lem6  9179  fpwwe2lem12  9315  genpnnp  9679  addsrmo  9746  mulsrmo  9747  hashfun  13032  hash2exprb  13058  rtrclreclem3  13590  summo  14237  fsum2dlem  14285  ntrivcvgmul  14415  prodmo  14447  fprod2dlem  14491  iscatd2  16107  gsumval3eu  18070  gsum2d2  18138  ptbasin  21128  txcls  21155  txbasval  21157  reconn  22367  phtpcer  22529  phtpcerOLD  22530  pcohtpy  22555  mbfi1flimlem  23208  mbfmullem  23211  itg2add  23245  fsumvma  24651  clwlkswlks  26048  usg2wlkonot  26172  2spontn0vne  26176  2spotdisj  26350  pconcon  30269  txscon  30279  dfpo2  30700  neibastop1  31326  itg2addnc  32433  riscer  32756  dalem62  33837  pellexlem5  36214  pellex  36216  iunrelexpuztr  36829  fzisoeu  38254  stoweidlem53  38746  stoweidlem56  38749  umgr3v3e3cycl  41349  conngrv2edg  41360
  Copyright terms: Public domain W3C validator