Theorem exlimdvv 1938

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  euotd  5514  opabssxpd  5724  dfpo2  6296  funopg  6583  fmptsnd  7167  tpres  7202  opreuopreu  8020  frxp2  8130  frxp3  8137  fundmen  9031  undomOLD  9060  ttrcltr  9711  infxpenc2  10017  zorn2lem6  10496  fpwwe2lem11  10636  genpnnp  11000  addsrmo  11068  mulsrmo  11069  hashfun  14397  hash2exprb  14432  rtrclreclem3  15007  summo  15663  fsum2dlem  15716  ntrivcvgmul  15848  prodmo  15880  fprod2dlem  15924  iscatd2  17625  gsumval3eu  19772  gsum2d2  19842  ptbasin  23081  txcls  23108  txbasval  23110  reconn  24344  phtpcer  24511  pcohtpy  24536  mbfi1flimlem  25240  mbfmullem  25243  itg2add  25277  fsumvma  26716  umgr3v3e3cycl  29437  conngrv2edg  29448  2ndresdju  31874  cusgracyclt3v  34147  pconnconn  34222  txsconn  34232  neibastop1  35244  itg2addnc  36542  riscer  36856  dalem62  38605  pellexlem5  41571  pellex  41573  nnoeomeqom  42062  iunrelexpuztr  42470  fzisoeu  44010  stoweidlem53  44769  stoweidlem56  44772  fundcmpsurinjpreimafv  46076  ichnreuop  46140