Theorem exlimdvv 1935

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  euotd  5456  opabssxpd  5666  dfpo2  6248  funopg  6520  fmptsnd  7109  tpres  7141  opreuopreu  7972  frxp2  8080  frxp3  8087  fundmen  8960  ttrcltr  9613  infxpenc2  9920  zorn2lem6  10399  fpwwe2lem11  10539  genpnnp  10903  addsrmo  10971  mulsrmo  10972  hashfun  14346  hash2exprb  14380  hash3tpexb  14403  rtrclreclem3  14969  summo  15626  fsum2dlem  15679  ntrivcvgmul  15811  prodmo  15845  fprod2dlem  15889  iscatd2  17589  gsumval3eu  19818  gsum2d2  19888  ptbasin  23493  txcls  23520  txbasval  23522  reconn  24745  phtpcer  24922  pcohtpy  24948  mbfi1flimlem  25651  mbfmullem  25654  itg2add  25688  fsumvma  27152  umgr3v3e3cycl  30166  conngrv2edg  30177  brab2d  32590  2ndresdju  32633  cusgracyclt3v  35221  pconnconn  35296  txsconn  35306  neibastop1  36424  itg2addnc  37734  riscer  38048  dalem62  39853  pellexlem5  42950  pellex  42952  nnoeomeqom  43429  iunrelexpuztr  43836  fzisoeu  45425  stoweidlem53  46175  stoweidlem56  46178  fundcmpsurinjpreimafv  47532  ichnreuop  47596  cycldlenngric  48052  brab2dd  48952