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  5461  opabssxpd  5671  dfpo2  6254  funopg  6526  fmptsnd  7117  tpres  7149  opreuopreu  7980  frxp2  8087  frxp3  8094  fundmen  8971  ttrcltr  9628  infxpenc2  9935  zorn2lem6  10414  fpwwe2lem11  10555  genpnnp  10919  addsrmo  10987  mulsrmo  10988  hashfun  14390  hash2exprb  14424  hash3tpexb  14447  rtrclreclem3  15013  summo  15670  fsum2dlem  15723  ntrivcvgmul  15858  prodmo  15892  fprod2dlem  15936  iscatd2  17638  gsumval3eu  19870  gsum2d2  19940  ptbasin  23552  txcls  23579  txbasval  23581  reconn  24804  phtpcer  24972  pcohtpy  24997  mbfi1flimlem  25699  mbfmullem  25702  itg2add  25736  fsumvma  27190  umgr3v3e3cycl  30269  conngrv2edg  30280  brab2d  32693  2ndresdju  32737  cusgracyclt3v  35354  pconnconn  35429  txsconn  35439  neibastop1  36557  cgsex2gd  37467  itg2addnc  38009  riscer  38323  dalem62  40194  pellexlem5  43279  pellex  43281  nnoeomeqom  43758  iunrelexpuztr  44164  fzisoeu  45751  stoweidlem53  46499  stoweidlem56  46502  fundcmpsurinjpreimafv  47880  ichnreuop  47944  cycldlenngric  48416  brab2dd  49315