Theorem exlimdvv 1934

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  euotd  5460  opabssxpd  5670  dfpo2  6248  funopg  6520  fmptsnd  7109  tpres  7141  opreuopreu  7976  frxp2  8084  frxp3  8091  fundmen  8963  ttrcltr  9631  infxpenc2  9935  zorn2lem6  10414  fpwwe2lem11  10554  genpnnp  10918  addsrmo  10986  mulsrmo  10987  hashfun  14362  hash2exprb  14396  hash3tpexb  14419  rtrclreclem3  14985  summo  15642  fsum2dlem  15695  ntrivcvgmul  15827  prodmo  15861  fprod2dlem  15905  iscatd2  17605  gsumval3eu  19801  gsum2d2  19871  ptbasin  23480  txcls  23507  txbasval  23509  reconn  24733  phtpcer  24910  pcohtpy  24936  mbfi1flimlem  25639  mbfmullem  25642  itg2add  25676  fsumvma  27140  umgr3v3e3cycl  30146  conngrv2edg  30157  brab2d  32568  2ndresdju  32606  cusgracyclt3v  35128  pconnconn  35203  txsconn  35213  neibastop1  36332  itg2addnc  37653  riscer  37967  dalem62  39713  pellexlem5  42806  pellex  42808  nnoeomeqom  43285  iunrelexpuztr  43692  fzisoeu  45282  stoweidlem53  46035  stoweidlem56  46038  fundcmpsurinjpreimafv  47393  ichnreuop  47457  cycldlenngric  47913  brab2dd  48813