Theorem exlimdvv 1935

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  euotd  5453  opabssxpd  5663  dfpo2  6243  funopg  6515  fmptsnd  7103  tpres  7135  opreuopreu  7966  frxp2  8074  frxp3  8081  fundmen  8953  ttrcltr  9606  infxpenc2  9910  zorn2lem6  10389  fpwwe2lem11  10529  genpnnp  10893  addsrmo  10961  mulsrmo  10962  hashfun  14341  hash2exprb  14375  hash3tpexb  14398  rtrclreclem3  14964  summo  15621  fsum2dlem  15674  ntrivcvgmul  15806  prodmo  15840  fprod2dlem  15884  iscatd2  17584  gsumval3eu  19814  gsum2d2  19884  ptbasin  23490  txcls  23517  txbasval  23519  reconn  24742  phtpcer  24919  pcohtpy  24945  mbfi1flimlem  25648  mbfmullem  25651  itg2add  25685  fsumvma  27149  umgr3v3e3cycl  30159  conngrv2edg  30170  brab2d  32583  2ndresdju  32626  cusgracyclt3v  35188  pconnconn  35263  txsconn  35273  neibastop1  36392  itg2addnc  37713  riscer  38027  dalem62  39772  pellexlem5  42865  pellex  42867  nnoeomeqom  43344  iunrelexpuztr  43751  fzisoeu  45340  stoweidlem53  46090  stoweidlem56  46093  fundcmpsurinjpreimafv  47438  ichnreuop  47502  cycldlenngric  47958  brab2dd  48858