Theorem exlimddv 1937

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

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

This theorem is referenced by:  vtocld  3520  fvmptdv2  6968  fprresex  8262  tfrlem9a  8327  erref  8666  domdifsn  9000  xpdom2  9012  enfixsn  9026  domunsn  9067  mapdom1  9082  sucdom2  9139  fineqvlem  9178  fissuni  9269  fipreima  9270  indexfi  9272  brwdom2  9490  wdomtr  9492  unwdomg  9501  unxpwdom  9506  infdifsn  9578  isinffi  9916  ac5num  9958  numacn  9971  acndom  9973  acndom2  9976  fodomacn  9978  infpss  10138  ssfin4  10232  domfin4  10233  enfin2i  10243  fin23lem31  10265  fin23lem41  10274  axcclem  10379  canthp1lem1  10575  canthp1  10577  winafp  10620  wun0  10641  prlem936  10970  supmul  12126  supxrre  13254  infxrre  13264  ixxub  13294  ixxlb  13295  hash1elsn  14306  relexpindlem  14998  isumltss  15783  eulerth  16722  ramub2  16954  mrieqv2d  17574  mreexexlem4d  17582  acsinfd  18491  acsdomd  18492  dfgrp3lem  18980  issubg2  19083  psgnunilem3  19437  sylow1lem4  19542  sylow3  19574  prmcyg  19835  ablfaclem3  20030  lbspss  21046  lsmcv  21108  cygzn  21537  lbslcic  21808  lmff  23257  tgcmp  23357  hauscmplem  23362  clsconn  23386  2ndcsep  23415  1stcelcls  23417  ptcnplem  23577  txcn  23582  fbdmn0  23790  ptcmplem2  24009  ptcmplem3  24010  tsmsxplem1  24109  met2ndci  24478  nmoid  24698  phtpcer  24962  phtpcco2  24967  cmetcau  25257  iscmet3lem2  25260  bcthlem4  25295  bcthlem5  25296  ovolicc2lem2  25487  vitali  25582  mbfimaopnlem  25624  limciun  25863  vieta1lem2  26287  tgldim0eq  28587  hpgerlem  28849  cusgrfi  29544  fusgrmaxsize  29550  minvecolem5  30968  n0limd  32557  foresf1o  32590  unidifsnel  32621  unidifsnne  32622  2ndimaxp  32735  aciunf1lem  32751  fsumiunle  32920  gsumwrd2dccatlem  33170  cycpmconjslem2  33248  cycpmconjs  33249  elrspunidl  33520  ssdifidlprm  33550  krullndrng  33573  qsdrng  33589  1arithidom  33629  1arithufdlem4  33639  dimcl  33779  lmimdim  33780  lmicdim  33781  lvecdim0i  33782  lvecdim0  33783  lssdimle  33784  dimpropd  33785  dimkerim  33804  fedgmul  33808  extdg1id  33843  locfinref  34018  esumcst  34240  esumiun  34271  unelldsys  34335  sigapildsys  34339  carsggect  34495  carsgclctunlem3  34497  erdsze2lem1  35416  erdsze2  35418  ptpconn  35446  cvmliftpht  35531  filnetlem3  36593  numiunnum  36683  exlimimd  37595  poimirlem32  37900  mblfinlem2  37906  mblfinlem3  37907  mblfinlem4  37908  sdclem1  37991  sstotbnd  38023  prdsbnd  38041  prdstotbnd  38042  heibor1lem  38057  bfp  38072  eqvrelref  38942  llnn0  39889  lplnn0N  39920  lvoln0N  39964  diaglbN  41428  diaintclN  41431  dibglbN  41539  dibintclN  41540  dihglblem2aN  41666  dihintcl  41717  dvh1dim  41815  sticksstones20  42533  eldioph2lem1  43114  eldioph2lem2  43115  rencldnfilem  43174  kelac1  43417  hbt  43484  cpcoll2d  44612  cncmpmax  45389  lptre2pt  45995  itgsubsticclem  46330  stoweidlem28  46383  stoweidlem31  46386  stoweidlem46  46401  stoweidlem53  46408  stoweidlem59  46414  uniimaelsetpreimafv  47753  iinfssc  49413  iinfsubc  49414  imaid  49510  uobrcl  49549  uobeq2  49757  thincciso4  49813  termcbas2  49838  termchom  49844  termcterm2  49870  euendfunc  49882  termcarweu  49884  diag1f1o  49890  diag2f1o  49893  termfucterm  49900  uobeqterm  49902  setrec1  50047