Theorem exlimdvv 1849

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

Syntax hints:   → wi 4  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  euotd  4900  funopg  5836  fmptsnd  6340  tpres  6371  opabex2  6997  fundmen  7916  undom  7933  infxpenc2  8728  zorn2lem6  9206  fpwwe2lem12  9342  genpnnp  9706  addsrmo  9773  mulsrmo  9774  hashfun  13084  hash2exprb  13110  rtrclreclem3  13648  summo  14295  fsum2dlem  14343  ntrivcvgmul  14473  prodmo  14505  fprod2dlem  14549  iscatd2  16165  gsumval3eu  18128  gsum2d2  18196  ptbasin  21190  txcls  21217  txbasval  21219  reconn  22439  phtpcer  22602  phtpcerOLD  22603  pcohtpy  22628  mbfi1flimlem  23295  mbfmullem  23298  itg2add  23332  fsumvma  24738  clwlkswlks  26286  usg2wlkonot  26410  2spontn0vne  26414  2spotdisj  26588  pconcon  30467  txscon  30477  dfpo2  30898  neibastop1  31524  itg2addnc  32634  riscer  32957  dalem62  34038  pellexlem5  36415  pellex  36417  iunrelexpuztr  37030  fzisoeu  38455  stoweidlem53  38946  stoweidlem56  38949  umgr3v3e3cycl  41351  conngrv2edg  41362