Theorem exlimdvv 1967

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2248. (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  5486  brab2d  5512  opabssxpd  5698  dfpo2  6292  funopg  6566  fmptsnd  7166  tpres  7199  opreuopreu  8035  frxp2  8145  frxp3  8152  fundmen  9043  ttrcltr  9701  infxpenc2  10082  zorn2lem6  10560  fpwwe2lem11  10707  genpnnp  11071  addsrmo  11139  mulsrmo  11140  hashfun  14562  hash2exprb  14596  hash3tpexb  14619  rtrclreclem3  15193  summo  15863  fsum2dlem  15916  ntrivcvgmul  16051  prodmo  16083  fprod2dlem  16127  iscatd2  17835  mgmn0plusgf  18807  mgmn0plusgplusf  18808  gsumval3eu  20098  gsum2d2  20168  ptbasin  23876  txcls  23903  txbasval  23905  reconn  25128  phtpcer  25296  pcohtpy  25321  mbfi1flimlem  26023  mbfmullem  26026  itg2add  26060  fsumvma  27522  umgr3v3e3cycl  30767  conngrv2edg  30778  2ndresdju  33225  cusgracyclt3v  35890  pconnconn  35965  txsconn  35975  neibastop1  37117  cgsex2gd  38026  itg2addnc  38560  riscer  38890  dalem62  40759  pellexlem5  43793  pellex  43795  nnoeomeqom  44272  iunrelexpuztr  44678  fzisoeu  46259  stoweidlem53  47007  stoweidlem56  47010  fundcmpsurinjpreimafv  48434  ichnreuop  48498  cycldlenngric  48970  brab2dd  49882