Theorem exlimddv 1936

Description: Existential elimination rule of natural deduction (Rule C, explained in exlimiv 1931). (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
exlimddv.1	⊢ (𝜑 → ∃𝑥𝜓)
exlimddv.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
exlimddv	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimddv

Step	Hyp	Ref	Expression
1		exlimddv.1	. 2 ⊢ (𝜑 → ∃𝑥𝜓)
2		exlimddv.2	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	2	ex 412	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	3	exlimdv 1934	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  vtocld  3518  fvmptdv2  6959  fprresex  8252  tfrlem9a  8317  erref  8655  domdifsn  8988  xpdom2  9000  enfixsn  9014  domunsn  9055  mapdom1  9070  sucdom2  9127  fineqvlem  9166  fissuni  9257  fipreima  9258  indexfi  9260  brwdom2  9478  wdomtr  9480  unwdomg  9489  unxpwdom  9494  infdifsn  9566  isinffi  9904  ac5num  9946  numacn  9959  acndom  9961  acndom2  9964  fodomacn  9966  infpss  10126  ssfin4  10220  domfin4  10221  enfin2i  10231  fin23lem31  10253  fin23lem41  10262  axcclem  10367  canthp1lem1  10563  canthp1  10565  winafp  10608  wun0  10629  prlem936  10958  supmul  12114  supxrre  13242  infxrre  13252  ixxub  13282  ixxlb  13283  hash1elsn  14294  relexpindlem  14986  isumltss  15771  eulerth  16710  ramub2  16942  mrieqv2d  17562  mreexexlem4d  17570  acsinfd  18479  acsdomd  18480  dfgrp3lem  18968  issubg2  19071  psgnunilem3  19425  sylow1lem4  19530  sylow3  19562  prmcyg  19823  ablfaclem3  20018  lbspss  21034  lsmcv  21096  cygzn  21525  lbslcic  21796  lmff  23245  tgcmp  23345  hauscmplem  23350  clsconn  23374  2ndcsep  23403  1stcelcls  23405  ptcnplem  23565  txcn  23570  fbdmn0  23778  ptcmplem2  23997  ptcmplem3  23998  tsmsxplem1  24097  met2ndci  24466  nmoid  24686  phtpcer  24950  phtpcco2  24955  cmetcau  25245  iscmet3lem2  25248  bcthlem4  25283  bcthlem5  25284  ovolicc2lem2  25475  vitali  25570  mbfimaopnlem  25612  limciun  25851  vieta1lem2  26275  tgldim0eq  28575  hpgerlem  28837  cusgrfi  29532  fusgrmaxsize  29538  minvecolem5  30956  n0limd  32546  foresf1o  32579  unidifsnel  32610  unidifsnne  32611  2ndimaxp  32724  aciunf1lem  32740  fsumiunle  32910  gsumwrd2dccatlem  33159  cycpmconjslem2  33237  cycpmconjs  33238  elrspunidl  33509  ssdifidlprm  33539  krullndrng  33562  qsdrng  33578  1arithidom  33618  1arithufdlem4  33628  dimcl  33759  lmimdim  33760  lmicdim  33761  lvecdim0i  33762  lvecdim0  33763  lssdimle  33764  dimpropd  33765  dimkerim  33784  fedgmul  33788  extdg1id  33823  locfinref  33998  esumcst  34220  esumiun  34251  unelldsys  34315  sigapildsys  34319  carsggect  34475  carsgclctunlem3  34477  erdsze2lem1  35397  erdsze2  35399  ptpconn  35427  cvmliftpht  35512  filnetlem3  36574  numiunnum  36664  exlimimd  37548  poimirlem32  37853  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  sdclem1  37944  sstotbnd  37976  prdsbnd  37994  prdstotbnd  37995  heibor1lem  38010  bfp  38025  eqvrelref  38867  llnn0  39776  lplnn0N  39807  lvoln0N  39851  diaglbN  41315  diaintclN  41318  dibglbN  41426  dibintclN  41427  dihglblem2aN  41553  dihintcl  41604  dvh1dim  41702  sticksstones20  42420  eldioph2lem1  43002  eldioph2lem2  43003  rencldnfilem  43062  kelac1  43305  hbt  43372  cpcoll2d  44500  cncmpmax  45277  lptre2pt  45884  itgsubsticclem  46219  stoweidlem28  46272  stoweidlem31  46275  stoweidlem46  46290  stoweidlem53  46297  stoweidlem59  46303  uniimaelsetpreimafv  47642  iinfssc  49302  iinfsubc  49303  imaid  49399  uobrcl  49438  uobeq2  49646  thincciso4  49702  termcbas2  49727  termchom  49733  termcterm2  49759  euendfunc  49771  termcarweu  49773  diag1f1o  49779  diag2f1o  49782  termfucterm  49789  uobeqterm  49791  setrec1  49936