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  5488  opabssxpd  5701  dfpo2  6285  funopg  6570  fmptsnd  7161  tpres  7193  opreuopreu  8033  frxp2  8143  frxp3  8150  fundmen  9045  undomOLD  9074  ttrcltr  9730  infxpenc2  10036  zorn2lem6  10515  fpwwe2lem11  10655  genpnnp  11019  addsrmo  11087  mulsrmo  11088  hashfun  14455  hash2exprb  14489  hash3tpexb  14512  rtrclreclem3  15079  summo  15733  fsum2dlem  15786  ntrivcvgmul  15918  prodmo  15952  fprod2dlem  15996  iscatd2  17693  gsumval3eu  19885  gsum2d2  19955  ptbasin  23515  txcls  23542  txbasval  23544  reconn  24768  phtpcer  24945  pcohtpy  24971  mbfi1flimlem  25675  mbfmullem  25678  itg2add  25712  fsumvma  27176  umgr3v3e3cycl  30165  conngrv2edg  30176  brab2d  32587  2ndresdju  32627  cusgracyclt3v  35178  pconnconn  35253  txsconn  35263  neibastop1  36377  itg2addnc  37698  riscer  38012  dalem62  39753  pellexlem5  42856  pellex  42858  nnoeomeqom  43336  iunrelexpuztr  43743  fzisoeu  45329  stoweidlem53  46082  stoweidlem56  46085  fundcmpsurinjpreimafv  47422  ichnreuop  47486  cycldlenngric  47941  brab2dd  48806