Theorem exlimdvv 1941

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

Syntax hints:   → wi 4  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  euotd  5461  opabssxpd  5672  dfpo2  6254  funopg  6526  fmptsnd  7120  tpres  7152  opreuopreu  7983  frxp2  8091  frxp3  8098  fundmen  8975  ttrcltr  9635  infxpenc2  9942  zorn2lem6  10421  fpwwe2lem11  10562  genpnnp  10926  addsrmo  10994  mulsrmo  10995  hashfun  14397  hash2exprb  14431  hash3tpexb  14454  rtrclreclem3  15020  summo  15677  fsum2dlem  15730  ntrivcvgmul  15865  prodmo  15899  fprod2dlem  15943  iscatd2  17645  gsumval3eu  19877  gsum2d2  19947  ptbasin  23567  txcls  23594  txbasval  23596  reconn  24819  phtpcer  24987  pcohtpy  25012  mbfi1flimlem  25714  mbfmullem  25717  itg2add  25751  fsumvma  27201  umgr3v3e3cycl  30279  conngrv2edg  30290  brab2d  32704  2ndresdju  32748  cusgracyclt3v  35391  pconnconn  35466  txsconn  35476  neibastop1  36594  cgsex2gd  37504  itg2addnc  38048  riscer  38362  dalem62  40233  pellexlem5  43285  pellex  43287  nnoeomeqom  43764  iunrelexpuztr  44170  fzisoeu  45755  stoweidlem53  46503  stoweidlem56  46506  fundcmpsurinjpreimafv  47890  ichnreuop  47954  cycldlenngric  48426  brab2dd  49325