Theorem exlimddv 1932

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776

This theorem is referenced by:  vtocld  3560  fvmptdv2  7033  fprresex  8333  wfrlem17OLD  8363  tfrlem9a  8424  erref  8763  domdifsn  9092  xpdom2  9105  enfixsn  9119  sucdom2OLD  9120  domunsn  9165  mapdom1  9180  sucdom2  9240  fineqvlem  9295  fissuni  9394  fipreima  9395  indexfi  9397  brwdom2  9610  wdomtr  9612  unwdomg  9621  unxpwdom  9626  infdifsn  9694  isinffi  10029  ac5num  10073  numacn  10086  acndom  10088  acndom2  10091  fodomacn  10093  infpss  10253  ssfin4  10347  domfin4  10348  enfin2i  10358  fin23lem31  10380  fin23lem41  10389  axcclem  10494  canthp1lem1  10689  canthp1  10691  winafp  10734  wun0  10755  prlem936  11084  supmul  12237  supxrre  13365  infxrre  13374  ixxub  13404  ixxlb  13405  hash1elsn  14406  relexpindlem  15098  isumltss  15880  eulerth  16816  ramub2  17047  mrieqv2d  17683  mreexexlem4d  17691  acsinfd  18613  acsdomd  18614  dfgrp3lem  19068  issubg2  19171  psgnunilem3  19528  sylow1lem4  19633  sylow3  19665  prmcyg  19926  ablfaclem3  20121  lbspss  21098  lsmcv  21160  cygzn  21606  lbslcic  21878  lmff  23324  tgcmp  23424  hauscmplem  23429  clsconn  23453  2ndcsep  23482  1stcelcls  23484  ptcnplem  23644  txcn  23649  fbdmn0  23857  ptcmplem2  24076  ptcmplem3  24077  tsmsxplem1  24176  met2ndci  24550  nmoid  24778  phtpcer  25040  phtpcco2  25045  cmetcau  25336  iscmet3lem2  25339  bcthlem4  25374  bcthlem5  25375  ovolicc2lem2  25566  vitali  25661  mbfimaopnlem  25703  limciun  25943  vieta1lem2  26367  tgldim0eq  28525  hpgerlem  28787  cusgrfi  29490  fusgrmaxsize  29496  minvecolem5  30909  n0limd  32500  foresf1o  32531  unidifsnel  32560  unidifsnne  32561  2ndimaxp  32662  aciunf1lem  32678  fsumiunle  32835  gsumwrd2dccatlem  33051  cycpmconjslem2  33157  cycpmconjs  33158  elrspunidl  33435  ssdifidlprm  33465  krullndrng  33488  qsdrng  33504  1arithidom  33544  1arithufdlem4  33554  dimcl  33629  lmimdim  33630  lmicdim  33631  lvecdim0i  33632  lvecdim0  33633  lssdimle  33634  dimpropd  33635  dimkerim  33654  fedgmul  33658  extdg1id  33690  locfinref  33801  esumcst  34043  esumiun  34074  unelldsys  34138  sigapildsys  34142  carsggect  34299  carsgclctunlem3  34301  erdsze2lem1  35187  erdsze2  35189  ptpconn  35217  cvmliftpht  35302  filnetlem3  36362  numiunnum  36452  exlimimd  37325  poimirlem32  37638  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  sdclem1  37729  sstotbnd  37761  prdsbnd  37779  prdstotbnd  37780  heibor1lem  37795  bfp  37810  eqvrelref  38591  llnn0  39498  lplnn0N  39529  lvoln0N  39573  diaglbN  41037  diaintclN  41040  dibglbN  41148  dibintclN  41149  dihglblem2aN  41275  dihintcl  41326  dvh1dim  41424  sticksstones20  42147  eldioph2lem1  42747  eldioph2lem2  42748  rencldnfilem  42807  kelac1  43051  hbt  43118  cpcoll2d  44254  cncmpmax  44969  lptre2pt  45595  itgsubsticclem  45930  stoweidlem28  45983  stoweidlem31  45986  stoweidlem46  46001  stoweidlem53  46008  stoweidlem59  46014  uniimaelsetpreimafv  47320  setrec1  48921