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

Theorem exlimdvv 2011
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2227. (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 2010 . 2 (𝜑 → (∃𝑦𝜓𝜒))
32exlimdv 2010 1 (𝜑 → (∃𝑥𝑦𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988
This theorem depends on definitions:  df-bi 197  df-ex 1854
This theorem is referenced by:  euotd  5123  opabssxpd  5493  funopg  6083  fmptsnd  6600  tpres  6631  fundmen  8197  undom  8215  infxpenc2  9055  zorn2lem6  9535  fpwwe2lem12  9675  genpnnp  10039  addsrmo  10106  mulsrmo  10107  hashfun  13436  hash2exprb  13465  rtrclreclem3  14019  summo  14667  fsum2dlem  14720  ntrivcvgmul  14853  prodmo  14885  fprod2dlem  14929  iscatd2  16563  gsumval3eu  18525  gsum2d2  18593  ptbasin  21602  txcls  21629  txbasval  21631  reconn  22852  phtpcer  23015  pcohtpy  23040  mbfi1flimlem  23708  mbfmullem  23711  itg2add  23745  fsumvma  25158  umgr3v3e3cycl  27357  conngrv2edg  27368  pconnconn  31541  txsconn  31551  dfpo2  31973  neibastop1  32681  itg2addnc  33795  riscer  34118  dalem62  35541  pellexlem5  37917  pellex  37919  iunrelexpuztr  38531  fzisoeu  40031  stoweidlem53  40791  stoweidlem56  40794
  Copyright terms: Public domain W3C validator