Theorem exlimdvv 1913

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

Syntax hints:   → wi 4  ∃wex 1762

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

This theorem depends on definitions:  df-bi 208  df-ex 1763

This theorem is referenced by:  euotd  5297  opabssxpd  5678  funopg  6262  fmptsnd  6797  tpres  6833  opreuopreu  7593  fundmen  8434  undom  8455  infxpenc2  9297  zorn2lem6  9772  fpwwe2lem12  9912  genpnnp  10276  addsrmo  10344  mulsrmo  10345  hashfun  13646  hash2exprb  13675  rtrclreclem3  14253  summo  14907  fsum2dlem  14958  ntrivcvgmul  15091  prodmo  15123  fprod2dlem  15167  iscatd2  16781  gsumval3eu  18745  gsum2d2  18814  ptbasin  21869  txcls  21896  txbasval  21898  reconn  23119  phtpcer  23282  pcohtpy  23307  mbfi1flimlem  24006  mbfmullem  24009  itg2add  24043  fsumvma  25471  umgr3v3e3cycl  27645  conngrv2edg  27656  cusgracyclt3v  32005  pconnconn  32080  txsconn  32090  dfpo2  32593  neibastop1  33310  itg2addnc  34490  riscer  34811  dalem62  36414  pellexlem5  38928  pellex  38930  iunrelexpuztr  39562  fzisoeu  41121  stoweidlem53  41894  stoweidlem56  41897  ichnreuop  43130