Theorem exlimdvv 1936

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912

This theorem depends on definitions:  df-bi 210  df-ex 1783

This theorem is referenced by:  euotd  5373  opabssxpd  5761  funopg  6370  fmptsnd  6923  tpres  6955  opreuopreu  7739  fundmen  8603  undom  8627  infxpenc2  9483  zorn2lem6  9962  fpwwe2lem11  10102  genpnnp  10466  addsrmo  10534  mulsrmo  10535  hashfun  13849  hash2exprb  13882  rtrclreclem3  14468  summo  15123  fsum2dlem  15174  ntrivcvgmul  15307  prodmo  15339  fprod2dlem  15383  iscatd2  17011  gsumval3eu  19093  gsum2d2  19163  ptbasin  22278  txcls  22305  txbasval  22307  reconn  23530  phtpcer  23697  pcohtpy  23722  mbfi1flimlem  24423  mbfmullem  24426  itg2add  24460  fsumvma  25897  umgr3v3e3cycl  28069  conngrv2edg  28080  2ndresdju  30510  cusgracyclt3v  32635  pconnconn  32710  txsconn  32720  dfpo2  33239  frxp2  33347  frxp3  33353  neibastop1  34098  itg2addnc  35392  riscer  35707  dalem62  37311  pellexlem5  40148  pellex  40150  iunrelexpuztr  40794  fzisoeu  42301  stoweidlem53  43062  stoweidlem56  43065  fundcmpsurinjpreimafv  44294  ichnreuop  44358