Theorem exlimdvv 1964

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

Syntax hints:   → wi 4  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  euotd  5498  brab2d  5524  opabssxpd  5710  dfpo2  6299  funopg  6572  fmptsnd  7169  tpres  7201  opreuopreu  8032  frxp2  8141  frxp3  8148  fundmen  9029  ttrcltr  9686  infxpenc2  10007  zorn2lem6  10486  fpwwe2lem11  10627  genpnnp  10991  addsrmo  11059  mulsrmo  11060  hashfun  14476  hash2exprb  14510  hash3tpexb  14533  rtrclreclem3  15099  summo  15770  fsum2dlem  15823  ntrivcvgmul  15958  prodmo  15992  fprod2dlem  16036  iscatd2  17738  gsumval3eu  19975  gsum2d2  20045  ptbasin  23715  txcls  23742  txbasval  23744  reconn  24967  phtpcer  25135  pcohtpy  25160  mbfi1flimlem  25862  mbfmullem  25865  itg2add  25899  fsumvma  27358  umgr3v3e3cycl  30516  conngrv2edg  30527  2ndresdju  32975  cusgracyclt3v  35629  pconnconn  35704  txsconn  35714  neibastop1  36851  cgsex2gd  37762  itg2addnc  38306  riscer  38620  dalem62  40489  pellexlem5  43543  pellex  43545  nnoeomeqom  44022  iunrelexpuztr  44428  fzisoeu  46002  stoweidlem53  46750  stoweidlem56  46753  fundcmpsurinjpreimafv  48140  ichnreuop  48204  cycldlenngric  48676  brab2dd  49589