Theorem exlimdvv 1957

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

Syntax hints:   → wi 4  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-ex 1803

This theorem is referenced by:  euotd  5486  brab2d  5512  opabssxpd  5698  dfpo2  6286  funopg  6559  fmptsnd  7157  tpres  7189  opreuopreu  8019  frxp2  8128  frxp3  8135  fundmen  9016  ttrcltr  9673  infxpenc2  9994  zorn2lem6  10473  fpwwe2lem11  10614  genpnnp  10978  addsrmo  11046  mulsrmo  11047  hashfun  14462  hash2exprb  14496  hash3tpexb  14519  rtrclreclem3  15085  summo  15756  fsum2dlem  15809  ntrivcvgmul  15944  prodmo  15978  fprod2dlem  16022  iscatd2  17725  gsumval3eu  19962  gsum2d2  20032  ptbasin  23691  txcls  23718  txbasval  23720  reconn  24943  phtpcer  25111  pcohtpy  25136  mbfi1flimlem  25838  mbfmullem  25841  itg2add  25875  fsumvma  27331  umgr3v3e3cycl  30440  conngrv2edg  30451  2ndresdju  32902  cusgracyclt3v  35514  pconnconn  35589  txsconn  35599  neibastop1  36727  cgsex2gd  37636  itg2addnc  38180  riscer  38494  dalem62  40365  pellexlem5  43417  pellex  43419  nnoeomeqom  43896  iunrelexpuztr  44302  fzisoeu  45878  stoweidlem53  46626  stoweidlem56  46629  fundcmpsurinjpreimafv  48013  ichnreuop  48077  cycldlenngric  48549  brab2dd  49458