Theorem exlimdvv 1934

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  euotd  5518  opabssxpd  5732  dfpo2  6316  funopg  6600  fmptsnd  7189  tpres  7221  opreuopreu  8059  frxp2  8169  frxp3  8176  fundmen  9071  undomOLD  9100  ttrcltr  9756  infxpenc2  10062  zorn2lem6  10541  fpwwe2lem11  10681  genpnnp  11045  addsrmo  11113  mulsrmo  11114  hashfun  14476  hash2exprb  14510  hash3tpexb  14533  rtrclreclem3  15099  summo  15753  fsum2dlem  15806  ntrivcvgmul  15938  prodmo  15972  fprod2dlem  16016  iscatd2  17724  gsumval3eu  19922  gsum2d2  19992  ptbasin  23585  txcls  23612  txbasval  23614  reconn  24850  phtpcer  25027  pcohtpy  25053  mbfi1flimlem  25757  mbfmullem  25760  itg2add  25794  fsumvma  27257  umgr3v3e3cycl  30203  conngrv2edg  30214  brab2d  32619  2ndresdju  32659  cusgracyclt3v  35161  pconnconn  35236  txsconn  35246  neibastop1  36360  itg2addnc  37681  riscer  37995  dalem62  39736  pellexlem5  42844  pellex  42846  nnoeomeqom  43325  iunrelexpuztr  43732  fzisoeu  45312  stoweidlem53  46068  stoweidlem56  46071  fundcmpsurinjpreimafv  47395  ichnreuop  47459  brab2dd  48741