Theorem exlimdvv 1938

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

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

This theorem is referenced by:  euotd  5513  opabssxpd  5722  dfpo2  6293  funopg  6580  fmptsnd  7164  tpres  7199  opreuopreu  8017  frxp2  8127  frxp3  8134  fundmen  9028  undomOLD  9057  ttrcltr  9708  infxpenc2  10014  zorn2lem6  10493  fpwwe2lem11  10633  genpnnp  10997  addsrmo  11065  mulsrmo  11066  hashfun  14394  hash2exprb  14429  rtrclreclem3  15004  summo  15660  fsum2dlem  15713  ntrivcvgmul  15845  prodmo  15877  fprod2dlem  15921  iscatd2  17622  gsumval3eu  19767  gsum2d2  19837  ptbasin  23073  txcls  23100  txbasval  23102  reconn  24336  phtpcer  24503  pcohtpy  24528  mbfi1flimlem  25232  mbfmullem  25235  itg2add  25269  fsumvma  26706  umgr3v3e3cycl  29427  conngrv2edg  29438  2ndresdju  31862  cusgracyclt3v  34136  pconnconn  34211  txsconn  34221  neibastop1  35233  itg2addnc  36531  riscer  36845  dalem62  38594  pellexlem5  41557  pellex  41559  nnoeomeqom  42048  iunrelexpuztr  42456  fzisoeu  43997  stoweidlem53  44756  stoweidlem56  44759  fundcmpsurinjpreimafv  46063  ichnreuop  46127