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 412	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	3	exlimdv 1937	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜒)

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

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  vtocld  3484  fvmptdv2  6875  fprresex  8097  wfrlem17OLD  8127  tfrlem9a  8188  erref  8476  domdifsn  8795  xpdom2  8807  enfixsn  8821  sucdom2  8822  domunsn  8863  mapdom1  8878  fineqvlem  8966  fissuni  9054  fipreima  9055  indexfi  9057  brwdom2  9262  wdomtr  9264  unwdomg  9273  unxpwdom  9278  infdifsn  9345  isinffi  9681  ac5num  9723  numacn  9736  acndom  9738  acndom2  9741  fodomacn  9743  infpss  9904  ssfin4  9997  domfin4  9998  enfin2i  10008  fin23lem31  10030  fin23lem41  10039  axcclem  10144  canthp1lem1  10339  canthp1  10341  winafp  10384  wun0  10405  prlem936  10734  supmul  11877  supxrre  12990  infxrre  12999  ixxub  13029  ixxlb  13030  hash1elsn  14014  relexpindlem  14702  isumltss  15488  eulerth  16412  ramub2  16643  mrieqv2d  17265  mreexexlem4d  17273  acsinfd  18189  acsdomd  18190  dfgrp3lem  18588  issubg2  18685  psgnunilem3  19019  sylow1lem4  19121  sylow3  19153  prmcyg  19410  ablfaclem3  19605  lbspss  20259  lsmcv  20318  cygzn  20690  lbslcic  20958  lmff  22360  tgcmp  22460  hauscmplem  22465  clsconn  22489  2ndcsep  22518  1stcelcls  22520  ptcnplem  22680  txcn  22685  fbdmn0  22893  ptcmplem2  23112  ptcmplem3  23113  tsmsxplem1  23212  met2ndci  23584  nmoid  23812  phtpcer  24064  phtpcco2  24068  cmetcau  24358  iscmet3lem2  24361  bcthlem4  24396  bcthlem5  24397  ovolicc2lem2  24587  vitali  24682  mbfimaopnlem  24724  limciun  24963  vieta1lem2  25376  tgldim0eq  26768  hpgerlem  27030  cusgrfi  27728  fusgrmaxsize  27734  minvecolem5  29144  foresf1o  30751  unidifsnel  30784  unidifsnne  30785  2ndimaxp  30885  aciunf1lem  30901  fsumiunle  31045  cycpmconjslem2  31324  cycpmconjs  31325  elrspunidl  31508  dimcl  31590  lvecdim0i  31591  lvecdim0  31592  lssdimle  31593  dimpropd  31594  dimkerim  31610  fedgmul  31614  extdg1id  31640  locfinref  31693  esumcst  31931  esumiun  31962  unelldsys  32026  sigapildsys  32030  carsggect  32185  carsgclctunlem3  32187  erdsze2lem1  33065  erdsze2  33067  ptpconn  33095  cvmliftpht  33180  filnetlem3  34496  exlimimd  35441  poimirlem32  35736  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  sdclem1  35828  sstotbnd  35860  prdsbnd  35878  prdstotbnd  35879  heibor1lem  35894  bfp  35909  eqvrelref  36650  llnn0  37457  lplnn0N  37488  lvoln0N  37532  diaglbN  38996  diaintclN  38999  dibglbN  39107  dibintclN  39108  dihglblem2aN  39234  dihintcl  39285  dvh1dim  39383  sticksstones20  40050  eldioph2lem1  40498  eldioph2lem2  40499  rencldnfilem  40558  kelac1  40804  hbt  40871  cpcoll2d  41766  cncmpmax  42464  lptre2pt  43071  itgsubsticclem  43406  stoweidlem28  43459  stoweidlem31  43462  stoweidlem46  43477  stoweidlem53  43484  stoweidlem59  43490  uniimaelsetpreimafv  44736  setrec1  46283