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

Syntax hints:   → wi 4   ∧ wa 399  ∃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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  fvmptdv2  6763  wfrlem17  7954  tfrlem9a  8005  erref  8292  domdifsn  8583  xpdom2  8595  enfixsn  8609  sucdom2  8610  domunsn  8651  mapdom1  8666  fineqvlem  8716  fissuni  8813  fipreima  8814  indexfi  8816  brwdom2  9021  wdomtr  9023  unwdomg  9032  unxpwdom  9037  infdifsn  9104  isinffi  9405  ac5num  9447  numacn  9460  acndom  9462  acndom2  9465  fodomacn  9467  infpss  9628  ssfin4  9721  domfin4  9722  enfin2i  9732  fin23lem31  9754  fin23lem41  9763  axcclem  9868  canthp1lem1  10063  canthp1  10065  winafp  10108  wun0  10129  prlem936  10458  supmul  11600  supxrre  12708  infxrre  12717  ixxub  12747  ixxlb  12748  hash1elsn  13728  relexpindlem  14414  isumltss  15195  eulerth  16110  ramub2  16340  mrieqv2d  16902  mreexexlem4d  16910  acsinfd  17782  acsdomd  17783  dfgrp3lem  18189  issubg2  18286  psgnunilem3  18616  sylow1lem4  18718  sylow3  18750  prmcyg  19007  ablfaclem3  19202  lbspss  19847  lsmcv  19906  cygzn  20262  lbslcic  20530  lmff  21906  tgcmp  22006  hauscmplem  22011  clsconn  22035  2ndcsep  22064  1stcelcls  22066  ptcnplem  22226  txcn  22231  fbdmn0  22439  ptcmplem2  22658  ptcmplem3  22659  tsmsxplem1  22758  met2ndci  23129  nmoid  23348  phtpcer  23600  phtpcco2  23604  cmetcau  23893  iscmet3lem2  23896  bcthlem4  23931  bcthlem5  23932  ovolicc2lem2  24122  vitali  24217  mbfimaopnlem  24259  limciun  24497  vieta1lem2  24907  tgldim0eq  26297  hpgerlem  26559  cusgrfi  27248  fusgrmaxsize  27254  minvecolem5  28664  foresf1o  30273  unidifsnel  30307  unidifsnne  30308  2ndimaxp  30409  aciunf1lem  30425  fsumiunle  30571  cycpmconjslem2  30847  cycpmconjs  30848  elrspunidl  31014  dimcl  31091  lvecdim0i  31092  lvecdim0  31093  lssdimle  31094  dimpropd  31095  dimkerim  31111  fedgmul  31115  extdg1id  31141  locfinref  31194  esumcst  31432  esumiun  31463  unelldsys  31527  sigapildsys  31531  carsggect  31686  carsgclctunlem3  31688  erdsze2lem1  32563  erdsze2  32565  ptpconn  32593  cvmliftpht  32678  filnetlem3  33841  exlimimd  34760  poimirlem32  35089  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  sdclem1  35181  sstotbnd  35213  prdsbnd  35231  prdstotbnd  35232  heibor1lem  35247  bfp  35262  eqvrelref  36005  llnn0  36812  lplnn0N  36843  lvoln0N  36887  diaglbN  38351  diaintclN  38354  dibglbN  38462  dibintclN  38463  dihglblem2aN  38589  dihintcl  38640  dvh1dim  38738  eldioph2lem1  39701  eldioph2lem2  39702  rencldnfilem  39761  kelac1  40007  hbt  40074  cpcoll2d  40967  cncmpmax  41661  lptre2pt  42282  itgsubsticclem  42617  stoweidlem28  42670  stoweidlem31  42673  stoweidlem46  42688  stoweidlem53  42695  stoweidlem59  42701  uniimaelsetpreimafv  43913  setrec1  45221