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  3515  fvmptdv2  6956  fprresex  8249  tfrlem9a  8314  erref  8651  domdifsn  8984  xpdom2  8996  enfixsn  9010  domunsn  9051  mapdom1  9066  sucdom2  9123  fineqvlem  9161  fissuni  9252  fipreima  9253  indexfi  9255  brwdom2  9470  wdomtr  9472  unwdomg  9481  unxpwdom  9486  infdifsn  9558  isinffi  9896  ac5num  9938  numacn  9951  acndom  9953  acndom2  9956  fodomacn  9958  infpss  10118  ssfin4  10212  domfin4  10213  enfin2i  10223  fin23lem31  10245  fin23lem41  10254  axcclem  10359  canthp1lem1  10554  canthp1  10556  winafp  10599  wun0  10620  prlem936  10949  supmul  12105  supxrre  13233  infxrre  13243  ixxub  13273  ixxlb  13274  hash1elsn  14285  relexpindlem  14977  isumltss  15762  eulerth  16701  ramub2  16933  mrieqv2d  17553  mreexexlem4d  17561  acsinfd  18470  acsdomd  18471  dfgrp3lem  18959  issubg2  19062  psgnunilem3  19416  sylow1lem4  19521  sylow3  19553  prmcyg  19814  ablfaclem3  20009  lbspss  21025  lsmcv  21087  cygzn  21516  lbslcic  21787  lmff  23236  tgcmp  23336  hauscmplem  23341  clsconn  23365  2ndcsep  23394  1stcelcls  23396  ptcnplem  23556  txcn  23561  fbdmn0  23769  ptcmplem2  23988  ptcmplem3  23989  tsmsxplem1  24088  met2ndci  24457  nmoid  24677  phtpcer  24941  phtpcco2  24946  cmetcau  25236  iscmet3lem2  25239  bcthlem4  25274  bcthlem5  25275  ovolicc2lem2  25466  vitali  25561  mbfimaopnlem  25603  limciun  25842  vieta1lem2  26266  tgldim0eq  28501  hpgerlem  28763  cusgrfi  29458  fusgrmaxsize  29464  minvecolem5  30882  n0limd  32472  foresf1o  32505  unidifsnel  32536  unidifsnne  32537  2ndimaxp  32650  aciunf1lem  32666  fsumiunle  32838  gsumwrd2dccatlem  33087  cycpmconjslem2  33165  cycpmconjs  33166  elrspunidl  33437  ssdifidlprm  33467  krullndrng  33490  qsdrng  33506  1arithidom  33546  1arithufdlem4  33556  dimcl  33687  lmimdim  33688  lmicdim  33689  lvecdim0i  33690  lvecdim0  33691  lssdimle  33692  dimpropd  33693  dimkerim  33712  fedgmul  33716  extdg1id  33751  locfinref  33926  esumcst  34148  esumiun  34179  unelldsys  34243  sigapildsys  34247  carsggect  34403  carsgclctunlem3  34405  erdsze2lem1  35319  erdsze2  35321  ptpconn  35349  cvmliftpht  35434  filnetlem3  36496  numiunnum  36586  exlimimd  37460  poimirlem32  37765  mblfinlem2  37771  mblfinlem3  37772  mblfinlem4  37773  sdclem1  37856  sstotbnd  37888  prdsbnd  37906  prdstotbnd  37907  heibor1lem  37922  bfp  37937  eqvrelref  38779  llnn0  39688  lplnn0N  39719  lvoln0N  39763  diaglbN  41227  diaintclN  41230  dibglbN  41338  dibintclN  41339  dihglblem2aN  41465  dihintcl  41516  dvh1dim  41614  sticksstones20  42332  eldioph2lem1  42917  eldioph2lem2  42918  rencldnfilem  42977  kelac1  43220  hbt  43287  cpcoll2d  44416  cncmpmax  45193  lptre2pt  45800  itgsubsticclem  46135  stoweidlem28  46188  stoweidlem31  46191  stoweidlem46  46206  stoweidlem53  46213  stoweidlem59  46219  uniimaelsetpreimafv  47558  iinfssc  49218  iinfsubc  49219  imaid  49315  uobrcl  49354  uobeq2  49562  thincciso4  49618  termcbas2  49643  termchom  49649  termcterm2  49675  euendfunc  49687  termcarweu  49689  diag1f1o  49695  diag2f1o  49698  termfucterm  49705  uobeqterm  49707  setrec1  49852