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  5467  opabssxpd  5678  dfpo2  6260  funopg  6532  fmptsnd  7124  tpres  7156  opreuopreu  7987  frxp2  8094  frxp3  8101  fundmen  8978  ttrcltr  9637  infxpenc2  9944  zorn2lem6  10423  fpwwe2lem11  10564  genpnnp  10928  addsrmo  10996  mulsrmo  10997  hashfun  14399  hash2exprb  14433  hash3tpexb  14456  rtrclreclem3  15022  summo  15679  fsum2dlem  15732  ntrivcvgmul  15867  prodmo  15901  fprod2dlem  15945  iscatd2  17647  gsumval3eu  19879  gsum2d2  19949  ptbasin  23542  txcls  23569  txbasval  23571  reconn  24794  phtpcer  24962  pcohtpy  24987  mbfi1flimlem  25689  mbfmullem  25692  itg2add  25726  fsumvma  27176  umgr3v3e3cycl  30254  conngrv2edg  30265  brab2d  32678  2ndresdju  32722  cusgracyclt3v  35338  pconnconn  35413  txsconn  35423  neibastop1  36541  cgsex2gd  37451  itg2addnc  37995  riscer  38309  dalem62  40180  pellexlem5  43261  pellex  43263  nnoeomeqom  43740  iunrelexpuztr  44146  fzisoeu  45733  stoweidlem53  46481  stoweidlem56  46484  fundcmpsurinjpreimafv  47868  ichnreuop  47932  cycldlenngric  48404  brab2dd  49303