Theorem exlimdvv 1934

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  euotd  5473  opabssxpd  5685  dfpo2  6269  funopg  6550  fmptsnd  7143  tpres  7175  opreuopreu  8013  frxp2  8123  frxp3  8130  fundmen  9002  ttrcltr  9669  infxpenc2  9975  zorn2lem6  10454  fpwwe2lem11  10594  genpnnp  10958  addsrmo  11026  mulsrmo  11027  hashfun  14402  hash2exprb  14436  hash3tpexb  14459  rtrclreclem3  15026  summo  15683  fsum2dlem  15736  ntrivcvgmul  15868  prodmo  15902  fprod2dlem  15946  iscatd2  17642  gsumval3eu  19834  gsum2d2  19904  ptbasin  23464  txcls  23491  txbasval  23493  reconn  24717  phtpcer  24894  pcohtpy  24920  mbfi1flimlem  25623  mbfmullem  25626  itg2add  25660  fsumvma  27124  umgr3v3e3cycl  30113  conngrv2edg  30124  brab2d  32535  2ndresdju  32573  cusgracyclt3v  35143  pconnconn  35218  txsconn  35228  neibastop1  36347  itg2addnc  37668  riscer  37982  dalem62  39728  pellexlem5  42821  pellex  42823  nnoeomeqom  43301  iunrelexpuztr  43708  fzisoeu  45298  stoweidlem53  46051  stoweidlem56  46054  fundcmpsurinjpreimafv  47409  ichnreuop  47473  cycldlenngric  47928  brab2dd  48816