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  3524  fvmptdv2  6968  fprresex  8266  tfrlem9a  8331  erref  8668  domdifsn  9001  xpdom2  9013  enfixsn  9027  domunsn  9068  mapdom1  9083  sucdom2  9144  fineqvlem  9185  fissuni  9284  fipreima  9285  indexfi  9287  brwdom2  9502  wdomtr  9504  unwdomg  9513  unxpwdom  9518  infdifsn  9586  isinffi  9921  ac5num  9965  numacn  9978  acndom  9980  acndom2  9983  fodomacn  9985  infpss  10145  ssfin4  10239  domfin4  10240  enfin2i  10250  fin23lem31  10272  fin23lem41  10281  axcclem  10386  canthp1lem1  10581  canthp1  10583  winafp  10626  wun0  10647  prlem936  10976  supmul  12131  supxrre  13263  infxrre  13273  ixxub  13303  ixxlb  13304  hash1elsn  14312  relexpindlem  15005  isumltss  15790  eulerth  16729  ramub2  16961  mrieqv2d  17576  mreexexlem4d  17584  acsinfd  18491  acsdomd  18492  dfgrp3lem  18946  issubg2  19049  psgnunilem3  19402  sylow1lem4  19507  sylow3  19539  prmcyg  19800  ablfaclem3  19995  lbspss  20965  lsmcv  21027  cygzn  21456  lbslcic  21726  lmff  23164  tgcmp  23264  hauscmplem  23269  clsconn  23293  2ndcsep  23322  1stcelcls  23324  ptcnplem  23484  txcn  23489  fbdmn0  23697  ptcmplem2  23916  ptcmplem3  23917  tsmsxplem1  24016  met2ndci  24386  nmoid  24606  phtpcer  24870  phtpcco2  24875  cmetcau  25165  iscmet3lem2  25168  bcthlem4  25203  bcthlem5  25204  ovolicc2lem2  25395  vitali  25490  mbfimaopnlem  25532  limciun  25771  vieta1lem2  26195  tgldim0eq  28406  hpgerlem  28668  cusgrfi  29362  fusgrmaxsize  29368  minvecolem5  30783  n0limd  32374  foresf1o  32406  unidifsnel  32437  unidifsnne  32438  2ndimaxp  32543  aciunf1lem  32559  fsumiunle  32727  gsumwrd2dccatlem  32979  cycpmconjslem2  33085  cycpmconjs  33086  elrspunidl  33372  ssdifidlprm  33402  krullndrng  33425  qsdrng  33441  1arithidom  33481  1arithufdlem4  33491  dimcl  33571  lmimdim  33572  lmicdim  33573  lvecdim0i  33574  lvecdim0  33575  lssdimle  33576  dimpropd  33577  dimkerim  33596  fedgmul  33600  extdg1id  33634  locfinref  33804  esumcst  34026  esumiun  34057  unelldsys  34121  sigapildsys  34125  carsggect  34282  carsgclctunlem3  34284  erdsze2lem1  35163  erdsze2  35165  ptpconn  35193  cvmliftpht  35278  filnetlem3  36341  numiunnum  36431  exlimimd  37304  poimirlem32  37619  mblfinlem2  37625  mblfinlem3  37626  mblfinlem4  37627  sdclem1  37710  sstotbnd  37742  prdsbnd  37760  prdstotbnd  37761  heibor1lem  37776  bfp  37791  eqvrelref  38574  llnn0  39483  lplnn0N  39514  lvoln0N  39558  diaglbN  41022  diaintclN  41025  dibglbN  41133  dibintclN  41134  dihglblem2aN  41260  dihintcl  41311  dvh1dim  41409  sticksstones20  42127  eldioph2lem1  42721  eldioph2lem2  42722  rencldnfilem  42781  kelac1  43025  hbt  43092  cpcoll2d  44221  cncmpmax  44999  lptre2pt  45611  itgsubsticclem  45946  stoweidlem28  45999  stoweidlem31  46002  stoweidlem46  46017  stoweidlem53  46024  stoweidlem59  46030  uniimaelsetpreimafv  47370  iinfssc  49019  iinfsubc  49020  imaid  49116  uobrcl  49155  uobeq2  49363  thincciso4  49419  termcbas2  49444  termchom  49450  termcterm2  49476  euendfunc  49488  termcarweu  49490  diag1f1o  49496  diag2f1o  49499  termfucterm  49506  uobeqterm  49508  setrec1  49653