Theorem exlimddv 1935

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  vtocld  3518  fvmptdv2  6952  fprresex  8250  tfrlem9a  8315  erref  8652  domdifsn  8984  xpdom2  8996  enfixsn  9010  domunsn  9051  mapdom1  9066  sucdom2  9127  fineqvlem  9167  fissuni  9266  fipreima  9267  indexfi  9269  brwdom2  9484  wdomtr  9486  unwdomg  9495  unxpwdom  9500  infdifsn  9572  isinffi  9907  ac5num  9949  numacn  9962  acndom  9964  acndom2  9967  fodomacn  9969  infpss  10129  ssfin4  10223  domfin4  10224  enfin2i  10234  fin23lem31  10256  fin23lem41  10265  axcclem  10370  canthp1lem1  10565  canthp1  10567  winafp  10610  wun0  10631  prlem936  10960  supmul  12115  supxrre  13247  infxrre  13257  ixxub  13287  ixxlb  13288  hash1elsn  14296  relexpindlem  14988  isumltss  15773  eulerth  16712  ramub2  16944  mrieqv2d  17563  mreexexlem4d  17571  acsinfd  18480  acsdomd  18481  dfgrp3lem  18935  issubg2  19038  psgnunilem3  19393  sylow1lem4  19498  sylow3  19530  prmcyg  19791  ablfaclem3  19986  lbspss  21004  lsmcv  21066  cygzn  21495  lbslcic  21766  lmff  23204  tgcmp  23304  hauscmplem  23309  clsconn  23333  2ndcsep  23362  1stcelcls  23364  ptcnplem  23524  txcn  23529  fbdmn0  23737  ptcmplem2  23956  ptcmplem3  23957  tsmsxplem1  24056  met2ndci  24426  nmoid  24646  phtpcer  24910  phtpcco2  24915  cmetcau  25205  iscmet3lem2  25208  bcthlem4  25243  bcthlem5  25244  ovolicc2lem2  25435  vitali  25530  mbfimaopnlem  25572  limciun  25811  vieta1lem2  26235  tgldim0eq  28466  hpgerlem  28728  cusgrfi  29422  fusgrmaxsize  29428  minvecolem5  30843  n0limd  32434  foresf1o  32466  unidifsnel  32497  unidifsnne  32498  2ndimaxp  32603  aciunf1lem  32619  fsumiunle  32787  gsumwrd2dccatlem  33032  cycpmconjslem2  33110  cycpmconjs  33111  elrspunidl  33378  ssdifidlprm  33408  krullndrng  33431  qsdrng  33447  1arithidom  33487  1arithufdlem4  33497  dimcl  33577  lmimdim  33578  lmicdim  33579  lvecdim0i  33580  lvecdim0  33581  lssdimle  33582  dimpropd  33583  dimkerim  33602  fedgmul  33606  extdg1id  33640  locfinref  33810  esumcst  34032  esumiun  34063  unelldsys  34127  sigapildsys  34131  carsggect  34288  carsgclctunlem3  34290  erdsze2lem1  35178  erdsze2  35180  ptpconn  35208  cvmliftpht  35293  filnetlem3  36356  numiunnum  36446  exlimimd  37319  poimirlem32  37634  mblfinlem2  37640  mblfinlem3  37641  mblfinlem4  37642  sdclem1  37725  sstotbnd  37757  prdsbnd  37775  prdstotbnd  37776  heibor1lem  37791  bfp  37806  eqvrelref  38589  llnn0  39498  lplnn0N  39529  lvoln0N  39573  diaglbN  41037  diaintclN  41040  dibglbN  41148  dibintclN  41149  dihglblem2aN  41275  dihintcl  41326  dvh1dim  41424  sticksstones20  42142  eldioph2lem1  42736  eldioph2lem2  42737  rencldnfilem  42796  kelac1  43039  hbt  43106  cpcoll2d  44235  cncmpmax  45013  lptre2pt  45625  itgsubsticclem  45960  stoweidlem28  46013  stoweidlem31  46016  stoweidlem46  46031  stoweidlem53  46038  stoweidlem59  46044  uniimaelsetpreimafv  47384  iinfssc  49046  iinfsubc  49047  imaid  49143  uobrcl  49182  uobeq2  49390  thincciso4  49446  termcbas2  49471  termchom  49477  termcterm2  49503  euendfunc  49515  termcarweu  49517  diag1f1o  49523  diag2f1o  49526  termfucterm  49533  uobeqterm  49535  setrec1  49680