Theorem exlimdvv 1931

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

Syntax hints:   → wi 4  ∃wex 1775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  euotd  5522  opabssxpd  5735  dfpo2  6317  funopg  6601  fmptsnd  7188  tpres  7220  opreuopreu  8057  frxp2  8167  frxp3  8174  fundmen  9069  undomOLD  9098  ttrcltr  9753  infxpenc2  10059  zorn2lem6  10538  fpwwe2lem11  10678  genpnnp  11042  addsrmo  11110  mulsrmo  11111  hashfun  14472  hash2exprb  14506  hash3tpexb  14529  rtrclreclem3  15095  summo  15749  fsum2dlem  15802  ntrivcvgmul  15934  prodmo  15968  fprod2dlem  16012  iscatd2  17725  gsumval3eu  19936  gsum2d2  20006  ptbasin  23600  txcls  23627  txbasval  23629  reconn  24863  phtpcer  25040  pcohtpy  25066  mbfi1flimlem  25771  mbfmullem  25774  itg2add  25808  fsumvma  27271  umgr3v3e3cycl  30212  conngrv2edg  30223  brab2d  32626  2ndresdju  32665  cusgracyclt3v  35140  pconnconn  35215  txsconn  35225  neibastop1  36341  itg2addnc  37660  riscer  37974  dalem62  39716  pellexlem5  42820  pellex  42822  nnoeomeqom  43301  iunrelexpuztr  43708  fzisoeu  45250  stoweidlem53  46008  stoweidlem56  46011  fundcmpsurinjpreimafv  47332  ichnreuop  47396