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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  vtocld  3514  fvmptdv2  6942  fprresex  8235  tfrlem9a  8300  erref  8637  domdifsn  8968  xpdom2  8980  enfixsn  8994  domunsn  9035  mapdom1  9050  sucdom2  9107  fineqvlem  9145  fissuni  9236  fipreima  9237  indexfi  9239  brwdom2  9454  wdomtr  9456  unwdomg  9465  unxpwdom  9470  infdifsn  9542  isinffi  9880  ac5num  9922  numacn  9935  acndom  9937  acndom2  9940  fodomacn  9942  infpss  10102  ssfin4  10196  domfin4  10197  enfin2i  10207  fin23lem31  10229  fin23lem41  10238  axcclem  10343  canthp1lem1  10538  canthp1  10540  winafp  10583  wun0  10604  prlem936  10933  supmul  12089  supxrre  13221  infxrre  13231  ixxub  13261  ixxlb  13262  hash1elsn  14273  relexpindlem  14965  isumltss  15750  eulerth  16689  ramub2  16921  mrieqv2d  17540  mreexexlem4d  17548  acsinfd  18457  acsdomd  18458  dfgrp3lem  18946  issubg2  19049  psgnunilem3  19403  sylow1lem4  19508  sylow3  19540  prmcyg  19801  ablfaclem3  19996  lbspss  21011  lsmcv  21073  cygzn  21502  lbslcic  21773  lmff  23211  tgcmp  23311  hauscmplem  23316  clsconn  23340  2ndcsep  23369  1stcelcls  23371  ptcnplem  23531  txcn  23536  fbdmn0  23744  ptcmplem2  23963  ptcmplem3  23964  tsmsxplem1  24063  met2ndci  24432  nmoid  24652  phtpcer  24916  phtpcco2  24921  cmetcau  25211  iscmet3lem2  25214  bcthlem4  25249  bcthlem5  25250  ovolicc2lem2  25441  vitali  25536  mbfimaopnlem  25578  limciun  25817  vieta1lem2  26241  tgldim0eq  28476  hpgerlem  28738  cusgrfi  29432  fusgrmaxsize  29438  minvecolem5  30853  n0limd  32443  foresf1o  32476  unidifsnel  32507  unidifsnne  32508  2ndimaxp  32620  aciunf1lem  32636  fsumiunle  32804  gsumwrd2dccatlem  33038  cycpmconjslem2  33116  cycpmconjs  33117  elrspunidl  33385  ssdifidlprm  33415  krullndrng  33438  qsdrng  33454  1arithidom  33494  1arithufdlem4  33504  dimcl  33607  lmimdim  33608  lmicdim  33609  lvecdim0i  33610  lvecdim0  33611  lssdimle  33612  dimpropd  33613  dimkerim  33632  fedgmul  33636  extdg1id  33671  locfinref  33846  esumcst  34068  esumiun  34099  unelldsys  34163  sigapildsys  34167  carsggect  34323  carsgclctunlem3  34325  erdsze2lem1  35239  erdsze2  35241  ptpconn  35269  cvmliftpht  35354  filnetlem3  36414  numiunnum  36504  exlimimd  37377  poimirlem32  37692  mblfinlem2  37698  mblfinlem3  37699  mblfinlem4  37700  sdclem1  37783  sstotbnd  37815  prdsbnd  37833  prdstotbnd  37834  heibor1lem  37849  bfp  37864  eqvrelref  38647  llnn0  39555  lplnn0N  39586  lvoln0N  39630  diaglbN  41094  diaintclN  41097  dibglbN  41205  dibintclN  41206  dihglblem2aN  41332  dihintcl  41383  dvh1dim  41481  sticksstones20  42199  eldioph2lem1  42793  eldioph2lem2  42794  rencldnfilem  42853  kelac1  43096  hbt  43163  cpcoll2d  44292  cncmpmax  45069  lptre2pt  45678  itgsubsticclem  46013  stoweidlem28  46066  stoweidlem31  46069  stoweidlem46  46084  stoweidlem53  46091  stoweidlem59  46097  uniimaelsetpreimafv  47427  iinfssc  49089  iinfsubc  49090  imaid  49186  uobrcl  49225  uobeq2  49433  thincciso4  49489  termcbas2  49514  termchom  49520  termcterm2  49546  euendfunc  49558  termcarweu  49560  diag1f1o  49566  diag2f1o  49569  termfucterm  49576  uobeqterm  49578  setrec1  49723