Theorem exlimdvv 1938

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2207. (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

Step	Hyp	Ref	Expression
1		exlimdvv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	exlimdv 1937	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → 𝜒))
3	2	exlimdv 1937	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  euotd  5421  opabssxpd  5625  dfpo2  6188  funopg  6452  fmptsnd  7023  tpres  7058  opreuopreu  7849  fundmen  8775  undom  8800  infxpenc2  9709  zorn2lem6  10188  fpwwe2lem11  10328  genpnnp  10692  addsrmo  10760  mulsrmo  10761  hashfun  14080  hash2exprb  14113  rtrclreclem3  14699  summo  15357  fsum2dlem  15410  ntrivcvgmul  15542  prodmo  15574  fprod2dlem  15618  iscatd2  17307  gsumval3eu  19420  gsum2d2  19490  ptbasin  22636  txcls  22663  txbasval  22665  reconn  23897  phtpcer  24064  pcohtpy  24089  mbfi1flimlem  24792  mbfmullem  24795  itg2add  24829  fsumvma  26266  umgr3v3e3cycl  28449  conngrv2edg  28460  2ndresdju  30887  cusgracyclt3v  33018  pconnconn  33093  txsconn  33103  ttrcltr  33702  frxp2  33718  frxp3  33724  neibastop1  34475  itg2addnc  35758  riscer  36073  dalem62  37675  pellexlem5  40571  pellex  40573  iunrelexpuztr  41216  fzisoeu  42729  stoweidlem53  43484  stoweidlem56  43487  fundcmpsurinjpreimafv  44748  ichnreuop  44812