Theorem exlimdvv 1969

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

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

This theorem is used by:  euotd  5491  brab2d  5517  opabssxpd  5703  dfpo2  6320  funopg  6597  fmptsnd  7200  tpres  7233  opreuopreu  8073  frxp2  8191  frxp3  8198  fundmen  9090  ttrcltr  9747  infxpenc2  10131  zorn2lem6  10609  fpwwe2lem11  10756  genpnnp  11120  addsrmo  11188  mulsrmo  11189  hashfun  14612  hash2exprb  14646  hash3tpexb  14669  rtrclreclem3  15245  summo  15915  fsum2dlem  15968  ntrivcvgmul  16103  prodmo  16135  fprod2dlem  16179  iscatd2  17887  mgmn0plusgf  18859  mgmn0plusgplusf  18860  gsumval3eu  20151  gsum2d2  20221  ptbasin  23929  txcls  23956  txbasval  23958  reconn  25181  phtpcer  25349  pcohtpy  25374  mbfi1flimlem  26076  mbfmullem  26079  itg2add  26113  fsumvma  27573  umgr3v3e3cycl  30818  conngrv2edg  30829  2ndresdju  33318  cusgracyclt3v  36091  pconnconn  36176  txsconn  36186  neibastop1  37338  cgsex2gd  38263  itg2addnc  38797  riscer  39125  dalem62  40994  pellexlem5  44044  pellex  44046  nnoeomeqom  44517  iunrelexpuztr  44922  fzisoeu  46531  stoweidlem53  47278  stoweidlem56  47281  fundcmpsurinjpreimafv  48705  ichnreuop  48769  cycldlenngric  49241  brab2dd  50154