Theorem exlimdvv 1957

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2249. (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 1956	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → 𝜒))
3	2	exlimdv 1956	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  euotd  5487  brab2d  5513  opabssxpd  5699  dfpo2  6287  funopg  6559  fmptsnd  7157  tpres  7189  opreuopreu  8019  frxp2  8128  frxp3  8135  fundmen  9016  ttrcltr  9673  infxpenc2  9994  zorn2lem6  10473  fpwwe2lem11  10614  genpnnp  10978  addsrmo  11046  mulsrmo  11047  hashfun  14464  hash2exprb  14498  hash3tpexb  14521  rtrclreclem3  15087  summo  15758  fsum2dlem  15811  ntrivcvgmul  15946  prodmo  15980  fprod2dlem  16024  iscatd2  17727  gsumval3eu  19965  gsum2d2  20035  ptbasin  23695  txcls  23722  txbasval  23724  reconn  24947  phtpcer  25115  pcohtpy  25140  mbfi1flimlem  25842  mbfmullem  25845  itg2add  25879  fsumvma  27335  umgr3v3e3cycl  30444  conngrv2edg  30455  2ndresdju  32906  cusgracyclt3v  35519  pconnconn  35594  txsconn  35604  neibastop1  36732  cgsex2gd  37641  itg2addnc  38185  riscer  38499  dalem62  40370  pellexlem5  43422  pellex  43424  nnoeomeqom  43901  iunrelexpuztr  44307  fzisoeu  45877  stoweidlem53  46625  stoweidlem56  46628  fundcmpsurinjpreimafv  48012  ichnreuop  48076  cycldlenngric  48548  brab2dd  49457