Theorem exlimddv 1962

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807

This theorem is referenced by:  vtocld  3536  n0limd  4315  fvmptdv2  7006  fprresex  8303  tfrlem9a  8369  erref  8711  domdifsn  9044  xpdom2  9056  enfixsn  9070  domunsn  9111  mapdom1  9126  sucdom2  9183  fineqvlem  9222  fissuni  9310  fipreima  9311  indexfi  9313  brwdom2  9531  wdomtr  9533  unwdomg  9542  unxpwdom  9547  infdifsn  9622  isinffi  9974  ac5num  10016  numacn  10029  acndom  10031  acndom2  10034  fodomacn  10036  infpss  10195  ssfin4  10290  domfin4  10291  enfin2i  10301  fin23lem31  10323  fin23lem41  10332  axcclem  10437  canthp1lem1  10633  canthp1  10635  winafp  10678  wun0  10699  prlem936  11028  supmul  12183  supxrre  13349  infxrre  13359  ixxub  13389  ixxlb  13390  hash1elsn  14403  relexpindlem  15096  isumltss  15898  eulerth  16838  ramub2  17070  mrieqv2d  17691  mreexexlem4d  17699  acsinfd  18608  acsdomd  18609  dfgrp3lem  19100  issubg2  19204  psgnunilem3  19562  sylow1lem4  19667  sylow3  19699  prmcyg  19960  ablfaclem3  20155  lbspss  21177  lsmcv  21239  ssdifidlprm  21451  cygzn  21685  lbslcic  21956  lmff  23423  tgcmp  23523  hauscmplem  23528  clsconn  23552  2ndcsep  23581  1stcelcls  23583  ptcnplem  23743  txcn  23748  fbdmn0  23956  ptcmplem2  24175  ptcmplem3  24176  tsmsxplem1  24275  met2ndci  24644  nmoid  24864  phtpcer  25119  phtpcco2  25123  cmetcau  25413  iscmet3lem2  25416  bcthlem4  25451  bcthlem5  25452  ovolicc2lem2  25642  vitali  25737  mbfimaopnlem  25779  limciun  26018  vieta1lem2  26437  tgldim0eq  28734  hpgerlem  29002  cusgrfi  29745  fusgrmaxsize  29751  minvecolem5  31170  foresf1o  32787  unidifsnel  32818  unidifsnne  32819  2ndimaxp  32928  aciunf1lem  32944  padct  33000  fsumiunle  33110  gsumwrd2dccatlem  33334  cycpmconjslem2  33412  cycpmconjs  33413  elrspunidl  33676  krullndrng  33704  qsdrng  33720  dflring3  33728  1arithidom  33768  1arithufdlem4  33778  dimcl  33934  lmimdim  33935  lmicdim  33936  lvecdim0i  33937  lvecdim0  33938  lssdimle  33939  dimpropd  33940  dimkerim  33958  fedgmul  33962  extdg1id  33997  locfinref  34172  esumcst  34394  esumiun  34425  unelldsys  34489  sigapildsys  34493  carsggect  34649  carsgclctunlem3  34651  erdsze2lem1  35590  erdsze2  35592  ptpconn  35620  cvmliftpht  35705  filnetlem3  36776  numiunnum  36866  exlimimd  37872  poimirlem32  38186  mblfinlem2  38192  mblfinlem3  38193  mblfinlem4  38194  sdclem1  38277  sstotbnd  38309  prdsbnd  38327  prdstotbnd  38328  heibor1lem  38343  bfp  38358  eqvrelref  39228  llnn0  40175  lplnn0N  40206  lvoln0N  40250  diaglbN  41714  diaintclN  41717  dibglbN  41825  dibintclN  41826  dihglblem2aN  41952  dihintcl  42003  dvh1dim  42101  sticksstones20  42818  eldioph2lem1  43376  eldioph2lem2  43377  rencldnfilem  43432  kelac1  43675  hbt  43742  cpcoll2d  44854  cncmpmax  45637  lptre2pt  46239  itgsubsticclem  46574  stoweidlem28  46627  stoweidlem31  46630  stoweidlem46  46645  stoweidlem53  46652  stoweidlem59  46658  uniimaelsetpreimafv  48027  iinfssc  49713  iinfsubc  49714  imaid  49810  uobrcl  49849  uobeq2  50057  thincciso4  50113  termcbas2  50138  termchom  50144  termcterm2  50170  euendfunc  50182  termcarweu  50184  diag1f1o  50190  diag2f1o  50193  termfucterm  50200  uobeqterm  50202  setrec1  50347