Theorem exlimdvv 2011

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

Syntax hints:   → wi 4  ∃wex 1853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988

This theorem depends on definitions:  df-bi 197  df-ex 1854

This theorem is referenced by:  euotd  5123  opabssxpd  5493  funopg  6083  fmptsnd  6600  tpres  6631  fundmen  8197  undom  8215  infxpenc2  9055  zorn2lem6  9535  fpwwe2lem12  9675  genpnnp  10039  addsrmo  10106  mulsrmo  10107  hashfun  13436  hash2exprb  13465  rtrclreclem3  14019  summo  14667  fsum2dlem  14720  ntrivcvgmul  14853  prodmo  14885  fprod2dlem  14929  iscatd2  16563  gsumval3eu  18525  gsum2d2  18593  ptbasin  21602  txcls  21629  txbasval  21631  reconn  22852  phtpcer  23015  pcohtpy  23040  mbfi1flimlem  23708  mbfmullem  23711  itg2add  23745  fsumvma  25158  umgr3v3e3cycl  27357  conngrv2edg  27368  pconnconn  31541  txsconn  31551  dfpo2  31973  neibastop1  32681  itg2addnc  33795  riscer  34118  dalem62  35541  pellexlem5  37917  pellex  37919  iunrelexpuztr  38531  fzisoeu  40031  stoweidlem53  40791  stoweidlem56  40794