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  6947  fprresex  8240  tfrlem9a  8305  erref  8642  domdifsn  8973  xpdom2  8985  enfixsn  8999  domunsn  9040  mapdom1  9055  sucdom2  9112  fineqvlem  9150  fissuni  9241  fipreima  9242  indexfi  9244  brwdom2  9459  wdomtr  9461  unwdomg  9470  unxpwdom  9475  infdifsn  9547  isinffi  9885  ac5num  9927  numacn  9940  acndom  9942  acndom2  9945  fodomacn  9947  infpss  10107  ssfin4  10201  domfin4  10202  enfin2i  10212  fin23lem31  10234  fin23lem41  10243  axcclem  10348  canthp1lem1  10543  canthp1  10545  winafp  10588  wun0  10609  prlem936  10938  supmul  12094  supxrre  13226  infxrre  13236  ixxub  13266  ixxlb  13267  hash1elsn  14278  relexpindlem  14970  isumltss  15755  eulerth  16694  ramub2  16926  mrieqv2d  17545  mreexexlem4d  17553  acsinfd  18462  acsdomd  18463  dfgrp3lem  18951  issubg2  19054  psgnunilem3  19408  sylow1lem4  19513  sylow3  19545  prmcyg  19806  ablfaclem3  20001  lbspss  21016  lsmcv  21078  cygzn  21507  lbslcic  21778  lmff  23216  tgcmp  23316  hauscmplem  23321  clsconn  23345  2ndcsep  23374  1stcelcls  23376  ptcnplem  23536  txcn  23541  fbdmn0  23749  ptcmplem2  23968  ptcmplem3  23969  tsmsxplem1  24068  met2ndci  24437  nmoid  24657  phtpcer  24921  phtpcco2  24926  cmetcau  25216  iscmet3lem2  25219  bcthlem4  25254  bcthlem5  25255  ovolicc2lem2  25446  vitali  25541  mbfimaopnlem  25583  limciun  25822  vieta1lem2  26246  tgldim0eq  28481  hpgerlem  28743  cusgrfi  29437  fusgrmaxsize  29443  minvecolem5  30861  n0limd  32451  foresf1o  32484  unidifsnel  32515  unidifsnne  32516  2ndimaxp  32628  aciunf1lem  32644  fsumiunle  32812  gsumwrd2dccatlem  33046  cycpmconjslem2  33124  cycpmconjs  33125  elrspunidl  33393  ssdifidlprm  33423  krullndrng  33446  qsdrng  33462  1arithidom  33502  1arithufdlem4  33512  dimcl  33615  lmimdim  33616  lmicdim  33617  lvecdim0i  33618  lvecdim0  33619  lssdimle  33620  dimpropd  33621  dimkerim  33640  fedgmul  33644  extdg1id  33679  locfinref  33854  esumcst  34076  esumiun  34107  unelldsys  34171  sigapildsys  34175  carsggect  34331  carsgclctunlem3  34333  erdsze2lem1  35247  erdsze2  35249  ptpconn  35277  cvmliftpht  35362  filnetlem3  36424  numiunnum  36514  exlimimd  37387  poimirlem32  37691  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  sdclem1  37782  sstotbnd  37814  prdsbnd  37832  prdstotbnd  37833  heibor1lem  37848  bfp  37863  eqvrelref  38705  llnn0  39614  lplnn0N  39645  lvoln0N  39689  diaglbN  41153  diaintclN  41156  dibglbN  41264  dibintclN  41265  dihglblem2aN  41391  dihintcl  41442  dvh1dim  41540  sticksstones20  42258  eldioph2lem1  42852  eldioph2lem2  42853  rencldnfilem  42912  kelac1  43155  hbt  43222  cpcoll2d  44351  cncmpmax  45128  lptre2pt  45737  itgsubsticclem  46072  stoweidlem28  46125  stoweidlem31  46128  stoweidlem46  46143  stoweidlem53  46150  stoweidlem59  46156  uniimaelsetpreimafv  47495  iinfssc  49157  iinfsubc  49158  imaid  49254  uobrcl  49293  uobeq2  49501  thincciso4  49557  termcbas2  49582  termchom  49588  termcterm2  49614  euendfunc  49626  termcarweu  49628  diag1f1o  49634  diag2f1o  49637  termfucterm  49644  uobeqterm  49646  setrec1  49791