Theorem exlimdvv 1935

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  euotd  5461  opabssxpd  5671  dfpo2  6254  funopg  6526  fmptsnd  7115  tpres  7147  opreuopreu  7978  frxp2  8086  frxp3  8093  fundmen  8968  ttrcltr  9625  infxpenc2  9932  zorn2lem6  10411  fpwwe2lem11  10552  genpnnp  10916  addsrmo  10984  mulsrmo  10985  hashfun  14360  hash2exprb  14394  hash3tpexb  14417  rtrclreclem3  14983  summo  15640  fsum2dlem  15693  ntrivcvgmul  15825  prodmo  15859  fprod2dlem  15903  iscatd2  17604  gsumval3eu  19833  gsum2d2  19903  ptbasin  23521  txcls  23548  txbasval  23550  reconn  24773  phtpcer  24950  pcohtpy  24976  mbfi1flimlem  25679  mbfmullem  25682  itg2add  25716  fsumvma  27180  umgr3v3e3cycl  30259  conngrv2edg  30270  brab2d  32683  2ndresdju  32727  cusgracyclt3v  35350  pconnconn  35425  txsconn  35435  neibastop1  36553  itg2addnc  37871  riscer  38185  dalem62  39990  pellexlem5  43071  pellex  43073  nnoeomeqom  43550  iunrelexpuztr  43956  fzisoeu  45544  stoweidlem53  46293  stoweidlem56  46296  fundcmpsurinjpreimafv  47650  ichnreuop  47714  cycldlenngric  48170  brab2dd  49069