Theorem exlimdvv 1967

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2249. (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  5494  brab2d  5520  opabssxpd  5706  dfpo2  6298  funopg  6571  fmptsnd  7171  tpres  7204  opreuopreu  8035  frxp2  8146  frxp3  8153  fundmen  9042  ttrcltr  9699  infxpenc2  10029  zorn2lem6  10507  fpwwe2lem11  10654  genpnnp  11018  addsrmo  11086  mulsrmo  11087  hashfun  14506  hash2exprb  14540  hash3tpexb  14563  rtrclreclem3  15137  summo  15807  fsum2dlem  15860  ntrivcvgmul  15995  prodmo  16029  fprod2dlem  16073  iscatd2  17775  mgmn0plusgf  18747  mgmn0plusgplusf  18748  gsumval3eu  20037  gsum2d2  20107  ptbasin  23809  txcls  23836  txbasval  23838  reconn  25061  phtpcer  25229  pcohtpy  25254  mbfi1flimlem  25956  mbfmullem  25959  itg2add  25993  fsumvma  27457  umgr3v3e3cycl  30672  conngrv2edg  30683  2ndresdju  33130  cusgracyclt3v  35743  pconnconn  35818  txsconn  35828  neibastop1  36986  cgsex2gd  37897  itg2addnc  38431  riscer  38746  dalem62  40615  pellexlem5  43682  pellex  43684  nnoeomeqom  44161  iunrelexpuztr  44567  fzisoeu  46141  stoweidlem53  46889  stoweidlem56  46892  fundcmpsurinjpreimafv  48316  ichnreuop  48380  cycldlenngric  48852  brab2dd  49764