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

Syntax hints:   → wi 4   ∧ wa 397  ∃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 398  df-ex 1783

This theorem is referenced by:  vtocld  3543  fvmptdv2  7017  fprresex  8295  wfrlem17OLD  8325  tfrlem9a  8386  erref  8723  domdifsn  9054  xpdom2  9067  enfixsn  9081  sucdom2OLD  9082  domunsn  9127  mapdom1  9142  sucdom2  9206  fineqvlem  9262  fissuni  9357  fipreima  9358  indexfi  9360  brwdom2  9568  wdomtr  9570  unwdomg  9579  unxpwdom  9584  infdifsn  9652  isinffi  9987  ac5num  10031  numacn  10044  acndom  10046  acndom2  10049  fodomacn  10051  infpss  10212  ssfin4  10305  domfin4  10306  enfin2i  10316  fin23lem31  10338  fin23lem41  10347  axcclem  10452  canthp1lem1  10647  canthp1  10649  winafp  10692  wun0  10713  prlem936  11042  supmul  12186  supxrre  13306  infxrre  13315  ixxub  13345  ixxlb  13346  hash1elsn  14331  relexpindlem  15010  isumltss  15794  eulerth  16716  ramub2  16947  mrieqv2d  17583  mreexexlem4d  17591  acsinfd  18509  acsdomd  18510  dfgrp3lem  18921  issubg2  19021  psgnunilem3  19364  sylow1lem4  19469  sylow3  19501  prmcyg  19762  ablfaclem3  19957  lbspss  20693  lsmcv  20754  cygzn  21126  lbslcic  21396  lmff  22805  tgcmp  22905  hauscmplem  22910  clsconn  22934  2ndcsep  22963  1stcelcls  22965  ptcnplem  23125  txcn  23130  fbdmn0  23338  ptcmplem2  23557  ptcmplem3  23558  tsmsxplem1  23657  met2ndci  24031  nmoid  24259  phtpcer  24511  phtpcco2  24515  cmetcau  24806  iscmet3lem2  24809  bcthlem4  24844  bcthlem5  24845  ovolicc2lem2  25035  vitali  25130  mbfimaopnlem  25172  limciun  25411  vieta1lem2  25824  tgldim0eq  27754  hpgerlem  28016  cusgrfi  28715  fusgrmaxsize  28721  minvecolem5  30134  foresf1o  31742  unidifsnel  31772  unidifsnne  31773  2ndimaxp  31872  aciunf1lem  31887  fsumiunle  32035  cycpmconjslem2  32314  cycpmconjs  32315  elrspunidl  32546  qsdrng  32611  dimcl  32688  lmimdim  32689  lvecdim0i  32690  lvecdim0  32691  lssdimle  32692  dimpropd  32693  dimkerim  32712  fedgmul  32716  extdg1id  32742  locfinref  32821  esumcst  33061  esumiun  33092  unelldsys  33156  sigapildsys  33160  carsggect  33317  carsgclctunlem3  33319  erdsze2lem1  34194  erdsze2  34196  ptpconn  34224  cvmliftpht  34309  filnetlem3  35265  exlimimd  36224  poimirlem32  36520  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  sdclem1  36611  sstotbnd  36643  prdsbnd  36661  prdstotbnd  36662  heibor1lem  36677  bfp  36692  eqvrelref  37480  llnn0  38387  lplnn0N  38418  lvoln0N  38462  diaglbN  39926  diaintclN  39929  dibglbN  40037  dibintclN  40038  dihglblem2aN  40164  dihintcl  40215  dvh1dim  40313  sticksstones20  40982  eldioph2lem1  41498  eldioph2lem2  41499  rencldnfilem  41558  kelac1  41805  hbt  41872  cpcoll2d  43018  cncmpmax  43716  lptre2pt  44356  itgsubsticclem  44691  stoweidlem28  44744  stoweidlem31  44747  stoweidlem46  44762  stoweidlem53  44769  stoweidlem59  44775  uniimaelsetpreimafv  46064  setrec1  47736