Theorem exlimdvv 1936

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  euotd  5459  opabssxpd  5669  dfpo2  6252  funopg  6524  fmptsnd  7115  tpres  7147  opreuopreu  7978  frxp2  8085  frxp3  8092  fundmen  8969  ttrcltr  9626  infxpenc2  9933  zorn2lem6  10412  fpwwe2lem11  10553  genpnnp  10917  addsrmo  10985  mulsrmo  10986  hashfun  14388  hash2exprb  14422  hash3tpexb  14445  rtrclreclem3  15011  summo  15668  fsum2dlem  15721  ntrivcvgmul  15856  prodmo  15890  fprod2dlem  15934  iscatd2  17636  gsumval3eu  19868  gsum2d2  19938  ptbasin  23551  txcls  23578  txbasval  23580  reconn  24803  phtpcer  24971  pcohtpy  24996  mbfi1flimlem  25698  mbfmullem  25701  itg2add  25735  fsumvma  27195  umgr3v3e3cycl  30274  conngrv2edg  30285  brab2d  32698  2ndresdju  32742  cusgracyclt3v  35359  pconnconn  35434  txsconn  35444  neibastop1  36562  cgsex2gd  37464  itg2addnc  38006  riscer  38320  dalem62  40191  pellexlem5  43276  pellex  43278  nnoeomeqom  43755  iunrelexpuztr  44161  fzisoeu  45748  stoweidlem53  46496  stoweidlem56  46499  fundcmpsurinjpreimafv  47865  ichnreuop  47929  cycldlenngric  48401  brab2dd  49300