Theorem exlimddv 1967

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  vtocld  3522  n0limd  4300  fvmptdv2  7013  fprresex  8332  tfrlem9a  8398  erref  8742  domdifsn  9083  xpdom2  9095  enfixsn  9109  domunsn  9150  mapdom1  9165  sucdom2  9222  fineqvlem  9261  fissuni  9350  fipreima  9351  indexfi  9353  brwdom2  9571  wdomtr  9573  unwdomg  9582  unxpwdom  9587  infdifsn  9662  setrec1  9976  isinffi  10077  ac5num  10119  numacn  10132  acndom  10134  acndom2  10137  fodomacn  10139  infpss  10298  ssfin4  10392  domfin4  10393  enfin2i  10403  fin23lem31  10425  fin23lem41  10434  axcclem  10539  canthp1lem1  10741  canthp1  10743  winafp  10786  wun0  10807  prlem936  11136  supmul  12293  supxrre  13461  infxrre  13471  ixxub  13501  ixxlb  13502  hash1elsn  14519  relexpindlem  15222  isumltss  16023  eulerth  16966  ramub2  17198  mrieqv2d  17819  mreexexlem4d  17827  acsinfd  18736  acsdomd  18737  dfgrp3lem  19254  issubg2  19358  psgnunilem3  19716  sylow1lem4  19821  sylow3  19853  prmcyg  20114  ablfaclem3  20309  lbspss  21363  lsmcv  21425  ssdifidlprm  21648  cygzn  21882  lbslcic  22153  lmff  23625  tgcmp  23725  hauscmplem  23730  clsconn  23754  2ndcsep  23784  1stcelcls  23786  ptcnplem  23946  txcn  23951  fbdmn0  24159  ptcmplem2  24378  ptcmplem3  24379  tsmsxplem1  24478  met2ndci  24847  nmoid  25067  phtpcer  25322  phtpcco2  25326  cmetcau  25616  iscmet3lem2  25619  bcthlem4  25654  bcthlem5  25655  ovolicc2lem2  25845  vitali  25940  mbfimaopnlem  25982  limciun  26220  vieta1lem2  26640  tgldim0eq  28972  hpgerlem  29249  cusgrfi  30045  fusgrmaxsize  30051  minvecolem5  31489  foresf1o  33148  unidifsnel  33179  unidifsnne  33180  2ndimaxp  33288  aciunf1lem  33304  padct  33358  fsumiunle  33467  gsumwrd2dccatlem  33685  cycpmconjslem2  33763  cycpmconjs  33764  elrspunidl  34025  krullndrng  34052  qsdrng  34068  dflring3  34076  1arithidom  34116  1arithufdlem4  34126  dimcl  34282  lmimdim  34283  lmicdim  34284  lvecdim0i  34285  lvecdim0  34286  lssdimle  34287  dimpropd  34288  dimkerim  34306  fedgmul  34310  extdg1id  34345  locfinref  34520  esumcst  34742  esumiun  34773  unelldsys  34838  sigapildsys  34842  omssubadd  34979  carsggect  34997  carsgclctunlem3  34999  erdsze2lem1  36055  erdsze2  36057  ptpconn  36085  cvmliftpht  36170  filnetlem3  37261  numiunnum  37351  exlimimd  38360  poimirlem32  38664  mblfinlem2  38670  mblfinlem3  38671  mblfinlem4  38672  sdclem1  38771  sstotbnd  38803  prdsbnd  38821  prdstotbnd  38822  heibor1lem  38837  bfp  38852  eqvrelref  39720  llnn0  40667  lplnn0N  40698  lvoln0N  40742  diaglbN  42206  diaintclN  42209  dibglbN  42317  dibintclN  42318  dihglblem2aN  42444  dihintcl  42495  dvh1dim  42593  sticksstones20  43310  eldioph2lem1  43865  eldioph2lem2  43866  rencldnfilem  43921  kelac1  44159  hbt  44226  cpcoll2d  45337  cncmpmax  46143  lptre2pt  46744  itgsubsticclem  47079  stoweidlem28  47132  stoweidlem31  47135  stoweidlem46  47150  stoweidlem53  47157  stoweidlem59  47163  tmachlem-franscan  48053  uniimaelsetpreimafv  48572  iinfssc  50265  iinfsubc  50266  imaid  50364  uobrcl  50403  uobeq2  50630  thincciso4  50686  termcbas2  50711  termchom  50717  termcterm2  50743  euendfunc  50755  termcarweu  50757  diag1f1o  50763  diag2f1o  50769  termfucterm  50776  uobeqterm  50778