Theorem exlimdvv 1953

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

Syntax hints:   → wi 4  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  euotd  5481  opabssxpd  5692  dfpo2  6279  funopg  6551  fmptsnd  7149  tpres  7181  opreuopreu  8011  frxp2  8119  frxp3  8126  fundmen  9008  ttrcltr  9668  infxpenc2  9975  zorn2lem6  10455  fpwwe2lem11  10596  genpnnp  10960  addsrmo  11028  mulsrmo  11029  hashfun  14447  hash2exprb  14481  hash3tpexb  14504  rtrclreclem3  15070  summo  15727  fsum2dlem  15780  ntrivcvgmul  15915  prodmo  15949  fprod2dlem  15993  iscatd2  17696  gsumval3eu  19927  gsum2d2  19997  ptbasin  23617  txcls  23644  txbasval  23646  reconn  24869  phtpcer  25037  pcohtpy  25062  mbfi1flimlem  25764  mbfmullem  25767  itg2add  25801  fsumvma  27254  umgr3v3e3cycl  30332  conngrv2edg  30343  brab2d  32757  2ndresdju  32801  cusgracyclt3v  35470  pconnconn  35545  txsconn  35555  neibastop1  36683  cgsex2gd  37593  itg2addnc  38137  riscer  38451  dalem62  40322  pellexlem5  43374  pellex  43376  nnoeomeqom  43853  iunrelexpuztr  44259  fzisoeu  45843  stoweidlem53  46591  stoweidlem56  46594  fundcmpsurinjpreimafv  47978  ichnreuop  48042  cycldlenngric  48514  brab2dd  49413