Theorem exlimdvv 1933

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

Syntax hints:   → wi 4  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  euotd  5532  opabssxpd  5747  dfpo2  6327  funopg  6612  fmptsnd  7203  tpres  7238  opreuopreu  8075  frxp2  8185  frxp3  8192  fundmen  9096  undomOLD  9126  ttrcltr  9785  infxpenc2  10091  zorn2lem6  10570  fpwwe2lem11  10710  genpnnp  11074  addsrmo  11142  mulsrmo  11143  hashfun  14486  hash2exprb  14520  hash3tpexb  14543  rtrclreclem3  15109  summo  15765  fsum2dlem  15818  ntrivcvgmul  15950  prodmo  15984  fprod2dlem  16028  iscatd2  17739  gsumval3eu  19946  gsum2d2  20016  ptbasin  23606  txcls  23633  txbasval  23635  reconn  24869  phtpcer  25046  pcohtpy  25072  mbfi1flimlem  25777  mbfmullem  25780  itg2add  25814  fsumvma  27275  umgr3v3e3cycl  30216  conngrv2edg  30227  brab2d  32629  2ndresdju  32667  cusgracyclt3v  35124  pconnconn  35199  txsconn  35209  neibastop1  36325  itg2addnc  37634  riscer  37948  dalem62  39691  pellexlem5  42789  pellex  42791  nnoeomeqom  43274  iunrelexpuztr  43681  fzisoeu  45215  stoweidlem53  45974  stoweidlem56  45977  fundcmpsurinjpreimafv  47282  ichnreuop  47346