Theorem exlimdvv 1937

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

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

This theorem is referenced by:  euotd  5427  opabssxpd  5634  dfpo2  6199  funopg  6468  fmptsnd  7041  tpres  7076  opreuopreu  7876  fundmen  8821  undomOLD  8847  ttrcltr  9474  infxpenc2  9778  zorn2lem6  10257  fpwwe2lem11  10397  genpnnp  10761  addsrmo  10829  mulsrmo  10830  hashfun  14152  hash2exprb  14185  rtrclreclem3  14771  summo  15429  fsum2dlem  15482  ntrivcvgmul  15614  prodmo  15646  fprod2dlem  15690  iscatd2  17390  gsumval3eu  19505  gsum2d2  19575  ptbasin  22728  txcls  22755  txbasval  22757  reconn  23991  phtpcer  24158  pcohtpy  24183  mbfi1flimlem  24887  mbfmullem  24890  itg2add  24924  fsumvma  26361  umgr3v3e3cycl  28548  conngrv2edg  28559  2ndresdju  30986  cusgracyclt3v  33118  pconnconn  33193  txsconn  33203  frxp2  33791  frxp3  33797  neibastop1  34548  itg2addnc  35831  riscer  36146  dalem62  37748  pellexlem5  40655  pellex  40657  iunrelexpuztr  41327  fzisoeu  42839  stoweidlem53  43594  stoweidlem56  43597  fundcmpsurinjpreimafv  44860  ichnreuop  44924