Theorem exlimdvv 1936

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  euotd  5469  opabssxpd  5679  dfpo2  6262  funopg  6534  fmptsnd  7125  tpres  7157  opreuopreu  7988  frxp2  8096  frxp3  8103  fundmen  8980  ttrcltr  9637  infxpenc2  9944  zorn2lem6  10423  fpwwe2lem11  10564  genpnnp  10928  addsrmo  10996  mulsrmo  10997  hashfun  14372  hash2exprb  14406  hash3tpexb  14429  rtrclreclem3  14995  summo  15652  fsum2dlem  15705  ntrivcvgmul  15837  prodmo  15871  fprod2dlem  15915  iscatd2  17616  gsumval3eu  19845  gsum2d2  19915  ptbasin  23533  txcls  23560  txbasval  23562  reconn  24785  phtpcer  24962  pcohtpy  24988  mbfi1flimlem  25691  mbfmullem  25694  itg2add  25728  fsumvma  27192  umgr3v3e3cycl  30271  conngrv2edg  30282  brab2d  32694  2ndresdju  32738  cusgracyclt3v  35369  pconnconn  35444  txsconn  35454  neibastop1  36572  cgsex2gd  37386  itg2addnc  37919  riscer  38233  dalem62  40104  pellexlem5  43184  pellex  43186  nnoeomeqom  43663  iunrelexpuztr  44069  fzisoeu  45656  stoweidlem53  46405  stoweidlem56  46408  fundcmpsurinjpreimafv  47762  ichnreuop  47826  cycldlenngric  48282  brab2dd  49181