Theorem exlimdvv 1934

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 1933	. 2 ⊢ (𝜑 → (∃𝑦𝜓 → 𝜒))
3	2	exlimdv 1933	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  euotd  5476  opabssxpd  5688  dfpo2  6272  funopg  6553  fmptsnd  7146  tpres  7178  opreuopreu  8016  frxp2  8126  frxp3  8133  fundmen  9005  undomOLD  9034  ttrcltr  9676  infxpenc2  9982  zorn2lem6  10461  fpwwe2lem11  10601  genpnnp  10965  addsrmo  11033  mulsrmo  11034  hashfun  14409  hash2exprb  14443  hash3tpexb  14466  rtrclreclem3  15033  summo  15690  fsum2dlem  15743  ntrivcvgmul  15875  prodmo  15909  fprod2dlem  15953  iscatd2  17649  gsumval3eu  19841  gsum2d2  19911  ptbasin  23471  txcls  23498  txbasval  23500  reconn  24724  phtpcer  24901  pcohtpy  24927  mbfi1flimlem  25630  mbfmullem  25633  itg2add  25667  fsumvma  27131  umgr3v3e3cycl  30120  conngrv2edg  30131  brab2d  32542  2ndresdju  32580  cusgracyclt3v  35150  pconnconn  35225  txsconn  35235  neibastop1  36354  itg2addnc  37675  riscer  37989  dalem62  39735  pellexlem5  42828  pellex  42830  nnoeomeqom  43308  iunrelexpuztr  43715  fzisoeu  45305  stoweidlem53  46058  stoweidlem56  46061  fundcmpsurinjpreimafv  47413  ichnreuop  47477  cycldlenngric  47932  brab2dd  48820