Theorem exlimdvv 1931

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

Syntax hints:   → wi 4  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-ex 1777

This theorem is referenced by:  euotd  5395  opabssxpd  5783  funopg  6383  fmptsnd  6925  tpres  6957  opreuopreu  7728  fundmen  8577  undom  8599  infxpenc2  9442  zorn2lem6  9917  fpwwe2lem12  10057  genpnnp  10421  addsrmo  10489  mulsrmo  10490  hashfun  13792  hash2exprb  13823  rtrclreclem3  14413  summo  15068  fsum2dlem  15119  ntrivcvgmul  15252  prodmo  15284  fprod2dlem  15328  iscatd2  16946  gsumval3eu  19018  gsum2d2  19088  ptbasin  22179  txcls  22206  txbasval  22208  reconn  23430  phtpcer  23593  pcohtpy  23618  mbfi1flimlem  24317  mbfmullem  24320  itg2add  24354  fsumvma  25783  umgr3v3e3cycl  27957  conngrv2edg  27968  cusgracyclt3v  32398  pconnconn  32473  txsconn  32483  dfpo2  32986  neibastop1  33702  itg2addnc  34940  riscer  35260  dalem62  36864  pellexlem5  39423  pellex  39425  iunrelexpuztr  40057  fzisoeu  41560  stoweidlem53  42332  stoweidlem56  42335  fundcmpsurinjpreimafv  43562  ichnreuop  43628