Theorem exlimddv 1935

Description: Existential elimination rule of natural deduction (Rule C, explained in exlimiv 1930). (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 1933	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395  ∃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-an 396  df-ex 1780

This theorem is referenced by:  vtocld  3561  fvmptdv2  7034  fprresex  8335  wfrlem17OLD  8365  tfrlem9a  8426  erref  8765  domdifsn  9094  xpdom2  9107  enfixsn  9121  sucdom2OLD  9122  domunsn  9167  mapdom1  9182  sucdom2  9243  fineqvlem  9298  fissuni  9397  fipreima  9398  indexfi  9400  brwdom2  9613  wdomtr  9615  unwdomg  9624  unxpwdom  9629  infdifsn  9697  isinffi  10032  ac5num  10076  numacn  10089  acndom  10091  acndom2  10094  fodomacn  10096  infpss  10256  ssfin4  10350  domfin4  10351  enfin2i  10361  fin23lem31  10383  fin23lem41  10392  axcclem  10497  canthp1lem1  10692  canthp1  10694  winafp  10737  wun0  10758  prlem936  11087  supmul  12240  supxrre  13369  infxrre  13378  ixxub  13408  ixxlb  13409  hash1elsn  14410  relexpindlem  15102  isumltss  15884  eulerth  16820  ramub2  17052  mrieqv2d  17682  mreexexlem4d  17690  acsinfd  18601  acsdomd  18602  dfgrp3lem  19056  issubg2  19159  psgnunilem3  19514  sylow1lem4  19619  sylow3  19651  prmcyg  19912  ablfaclem3  20107  lbspss  21081  lsmcv  21143  cygzn  21589  lbslcic  21861  lmff  23309  tgcmp  23409  hauscmplem  23414  clsconn  23438  2ndcsep  23467  1stcelcls  23469  ptcnplem  23629  txcn  23634  fbdmn0  23842  ptcmplem2  24061  ptcmplem3  24062  tsmsxplem1  24161  met2ndci  24535  nmoid  24763  phtpcer  25027  phtpcco2  25032  cmetcau  25323  iscmet3lem2  25326  bcthlem4  25361  bcthlem5  25362  ovolicc2lem2  25553  vitali  25648  mbfimaopnlem  25690  limciun  25929  vieta1lem2  26353  tgldim0eq  28511  hpgerlem  28773  cusgrfi  29476  fusgrmaxsize  29482  minvecolem5  30900  n0limd  32491  foresf1o  32523  unidifsnel  32553  unidifsnne  32554  2ndimaxp  32656  aciunf1lem  32672  fsumiunle  32831  gsumwrd2dccatlem  33069  cycpmconjslem2  33175  cycpmconjs  33176  elrspunidl  33456  ssdifidlprm  33486  krullndrng  33509  qsdrng  33525  1arithidom  33565  1arithufdlem4  33575  dimcl  33653  lmimdim  33654  lmicdim  33655  lvecdim0i  33656  lvecdim0  33657  lssdimle  33658  dimpropd  33659  dimkerim  33678  fedgmul  33682  extdg1id  33716  locfinref  33840  esumcst  34064  esumiun  34095  unelldsys  34159  sigapildsys  34163  carsggect  34320  carsgclctunlem3  34322  erdsze2lem1  35208  erdsze2  35210  ptpconn  35238  cvmliftpht  35323  filnetlem3  36381  numiunnum  36471  exlimimd  37344  poimirlem32  37659  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  sdclem1  37750  sstotbnd  37782  prdsbnd  37800  prdstotbnd  37801  heibor1lem  37816  bfp  37831  eqvrelref  38611  llnn0  39518  lplnn0N  39549  lvoln0N  39593  diaglbN  41057  diaintclN  41060  dibglbN  41168  dibintclN  41169  dihglblem2aN  41295  dihintcl  41346  dvh1dim  41444  sticksstones20  42167  eldioph2lem1  42771  eldioph2lem2  42772  rencldnfilem  42831  kelac1  43075  hbt  43142  cpcoll2d  44278  cncmpmax  45037  lptre2pt  45655  itgsubsticclem  45990  stoweidlem28  46043  stoweidlem31  46046  stoweidlem46  46061  stoweidlem53  46068  stoweidlem59  46074  uniimaelsetpreimafv  47383  thincciso4  49106  termcterm2  49146  setrec1  49210