Theorem exlimddv 1939

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  vtocld  3495  fvmptdv2  6902  fprresex  8135  wfrlem17OLD  8165  tfrlem9a  8226  erref  8527  domdifsn  8850  xpdom2  8863  enfixsn  8877  sucdom2OLD  8878  domunsn  8923  mapdom1  8938  sucdom2  8998  fineqvlem  9046  fissuni  9133  fipreima  9134  indexfi  9136  brwdom2  9341  wdomtr  9343  unwdomg  9352  unxpwdom  9357  infdifsn  9424  isinffi  9759  ac5num  9801  numacn  9814  acndom  9816  acndom2  9819  fodomacn  9821  infpss  9982  ssfin4  10075  domfin4  10076  enfin2i  10086  fin23lem31  10108  fin23lem41  10117  axcclem  10222  canthp1lem1  10417  canthp1  10419  winafp  10462  wun0  10483  prlem936  10812  supmul  11956  supxrre  13070  infxrre  13079  ixxub  13109  ixxlb  13110  hash1elsn  14095  relexpindlem  14783  isumltss  15569  eulerth  16493  ramub2  16724  mrieqv2d  17357  mreexexlem4d  17365  acsinfd  18283  acsdomd  18284  dfgrp3lem  18682  issubg2  18779  psgnunilem3  19113  sylow1lem4  19215  sylow3  19247  prmcyg  19504  ablfaclem3  19699  lbspss  20353  lsmcv  20412  cygzn  20787  lbslcic  21057  lmff  22461  tgcmp  22561  hauscmplem  22566  clsconn  22590  2ndcsep  22619  1stcelcls  22621  ptcnplem  22781  txcn  22786  fbdmn0  22994  ptcmplem2  23213  ptcmplem3  23214  tsmsxplem1  23313  met2ndci  23687  nmoid  23915  phtpcer  24167  phtpcco2  24171  cmetcau  24462  iscmet3lem2  24465  bcthlem4  24500  bcthlem5  24501  ovolicc2lem2  24691  vitali  24786  mbfimaopnlem  24828  limciun  25067  vieta1lem2  25480  tgldim0eq  26873  hpgerlem  27135  cusgrfi  27834  fusgrmaxsize  27840  minvecolem5  29252  foresf1o  30859  unidifsnel  30892  unidifsnne  30893  2ndimaxp  30993  aciunf1lem  31008  fsumiunle  31152  cycpmconjslem2  31431  cycpmconjs  31432  elrspunidl  31615  dimcl  31697  lvecdim0i  31698  lvecdim0  31699  lssdimle  31700  dimpropd  31701  dimkerim  31717  fedgmul  31721  extdg1id  31747  locfinref  31800  esumcst  32040  esumiun  32071  unelldsys  32135  sigapildsys  32139  carsggect  32294  carsgclctunlem3  32296  erdsze2lem1  33174  erdsze2  33176  ptpconn  33204  cvmliftpht  33289  filnetlem3  34578  exlimimd  35523  poimirlem32  35818  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  sdclem1  35910  sstotbnd  35942  prdsbnd  35960  prdstotbnd  35961  heibor1lem  35976  bfp  35991  eqvrelref  36730  llnn0  37537  lplnn0N  37568  lvoln0N  37612  diaglbN  39076  diaintclN  39079  dibglbN  39187  dibintclN  39188  dihglblem2aN  39314  dihintcl  39365  dvh1dim  39463  sticksstones20  40129  eldioph2lem1  40589  eldioph2lem2  40590  rencldnfilem  40649  kelac1  40895  hbt  40962  cpcoll2d  41884  cncmpmax  42582  lptre2pt  43188  itgsubsticclem  43523  stoweidlem28  43576  stoweidlem31  43579  stoweidlem46  43594  stoweidlem53  43601  stoweidlem59  43607  uniimaelsetpreimafv  44859  setrec1  46408