Theorem exlimdvv 1966

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  euotd  5485  brab2d  5511  opabssxpd  5697  dfpo2  6299  funopg  6575  fmptsnd  7175  tpres  7208  opreuopreu  8047  frxp2  8164  frxp3  8171  fundmen  9063  ttrcltr  9721  infxpenc2  10105  zorn2lem6  10583  fpwwe2lem11  10730  genpnnp  11094  addsrmo  11162  mulsrmo  11163  hashfun  14586  hash2exprb  14620  hash3tpexb  14643  rtrclreclem3  15219  summo  15889  fsum2dlem  15942  ntrivcvgmul  16077  prodmo  16109  fprod2dlem  16153  iscatd2  17861  mgmn0plusgf  18833  mgmn0plusgplusf  18834  gsumval3eu  20124  gsum2d2  20194  ptbasin  23902  txcls  23929  txbasval  23931  reconn  25154  phtpcer  25322  pcohtpy  25347  mbfi1flimlem  26049  mbfmullem  26052  itg2add  26086  fsumvma  27546  umgr3v3e3cycl  30791  conngrv2edg  30802  2ndresdju  33291  cusgracyclt3v  35998  pconnconn  36083  txsconn  36093  neibastop1  37240  cgsex2gd  38152  itg2addnc  38686  riscer  39016  dalem62  40885  pellexlem5  43934  pellex  43936  nnoeomeqom  44408  iunrelexpuztr  44813  fzisoeu  46410  stoweidlem53  47157  stoweidlem56  47160  fundcmpsurinjpreimafv  48584  ichnreuop  48648  cycldlenngric  49120  brab2dd  50033