Theorem exlimdvv 1967

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

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

This theorem is used by:  euotd  5501  brab2d  5527  opabssxpd  5713  dfpo2  6304  funopg  6577  fmptsnd  7174  tpres  7206  opreuopreu  8040  frxp2  8149  frxp3  8156  fundmen  9038  ttrcltr  9695  infxpenc2  10025  zorn2lem6  10503  fpwwe2lem11  10644  genpnnp  11008  addsrmo  11076  mulsrmo  11077  hashfun  14494  hash2exprb  14528  hash3tpexb  14551  rtrclreclem3  15123  summo  15794  fsum2dlem  15847  ntrivcvgmul  15982  prodmo  16016  fprod2dlem  16060  iscatd2  17762  gsumval3eu  20005  gsum2d2  20075  ptbasin  23771  txcls  23798  txbasval  23800  reconn  25023  phtpcer  25191  pcohtpy  25216  mbfi1flimlem  25918  mbfmullem  25921  itg2add  25955  fsumvma  27414  umgr3v3e3cycl  30572  conngrv2edg  30583  2ndresdju  33031  cusgracyclt3v  35669  pconnconn  35744  txsconn  35754  neibastop1  36911  cgsex2gd  37822  itg2addnc  38366  riscer  38680  dalem62  40549  pellexlem5  43601  pellex  43603  nnoeomeqom  44080  iunrelexpuztr  44486  fzisoeu  46060  stoweidlem53  46808  stoweidlem56  46811  fundcmpsurinjpreimafv  48198  ichnreuop  48262  cycldlenngric  48734  brab2dd  49647