Theorem exlimddv 1968

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  vtocld  3523  n0limd  4301  fvmptdv2  7013  fprresex  8329  tfrlem9a  8395  erref  8739  domdifsn  9080  xpdom2  9092  enfixsn  9106  domunsn  9147  mapdom1  9162  sucdom2  9219  fineqvlem  9258  fissuni  9347  fipreima  9348  indexfi  9350  brwdom2  9568  wdomtr  9570  unwdomg  9579  unxpwdom  9584  infdifsn  9659  setrec1  9973  isinffi  10074  ac5num  10116  numacn  10129  acndom  10131  acndom2  10134  fodomacn  10136  infpss  10295  ssfin4  10389  domfin4  10390  enfin2i  10400  fin23lem31  10422  fin23lem41  10431  axcclem  10536  canthp1lem1  10738  canthp1  10740  winafp  10783  wun0  10804  prlem936  11133  supmul  12290  supxrre  13458  infxrre  13468  ixxub  13498  ixxlb  13499  hash1elsn  14516  relexpindlem  15217  isumltss  16018  eulerth  16961  ramub2  17193  mrieqv2d  17814  mreexexlem4d  17822  acsinfd  18731  acsdomd  18732  dfgrp3lem  19249  issubg2  19353  psgnunilem3  19711  sylow1lem4  19816  sylow3  19848  prmcyg  20109  ablfaclem3  20304  lbspss  21358  lsmcv  21420  ssdifidlprm  21643  cygzn  21877  lbslcic  22148  lmff  23620  tgcmp  23720  hauscmplem  23725  clsconn  23749  2ndcsep  23779  1stcelcls  23781  ptcnplem  23941  txcn  23946  fbdmn0  24154  ptcmplem2  24373  ptcmplem3  24374  tsmsxplem1  24473  met2ndci  24842  nmoid  25062  phtpcer  25317  phtpcco2  25321  cmetcau  25611  iscmet3lem2  25614  bcthlem4  25649  bcthlem5  25650  ovolicc2lem2  25840  vitali  25935  mbfimaopnlem  25977  limciun  26215  vieta1lem2  26635  tgldim0eq  28967  hpgerlem  29244  cusgrfi  30040  fusgrmaxsize  30046  minvecolem5  31484  foresf1o  33101  unidifsnel  33132  unidifsnne  33133  2ndimaxp  33241  aciunf1lem  33257  padct  33311  fsumiunle  33421  gsumwrd2dccatlem  33639  cycpmconjslem2  33717  cycpmconjs  33718  elrspunidl  33979  krullndrng  34006  qsdrng  34022  dflring3  34030  1arithidom  34070  1arithufdlem4  34080  dimcl  34236  lmimdim  34237  lmicdim  34238  lvecdim0i  34239  lvecdim0  34240  lssdimle  34241  dimpropd  34242  dimkerim  34260  fedgmul  34264  extdg1id  34299  locfinref  34474  esumcst  34696  esumiun  34727  unelldsys  34792  sigapildsys  34796  carsggect  34951  carsgclctunlem3  34953  erdsze2lem1  35969  erdsze2  35971  ptpconn  35999  cvmliftpht  36084  filnetlem3  37169  numiunnum  37259  exlimimd  38268  poimirlem32  38572  mblfinlem2  38578  mblfinlem3  38579  mblfinlem4  38580  sdclem1  38679  sstotbnd  38711  prdsbnd  38729  prdstotbnd  38730  heibor1lem  38745  bfp  38760  eqvrelref  39628  llnn0  40575  lplnn0N  40606  lvoln0N  40650  diaglbN  42114  diaintclN  42117  dibglbN  42225  dibintclN  42226  dihglblem2aN  42352  dihintcl  42403  dvh1dim  42501  sticksstones20  43218  eldioph2lem1  43772  eldioph2lem2  43773  rencldnfilem  43828  kelac1  44066  hbt  44133  cpcoll2d  45244  cncmpmax  46050  lptre2pt  46651  itgsubsticclem  46986  stoweidlem28  47039  stoweidlem31  47042  stoweidlem46  47057  stoweidlem53  47064  stoweidlem59  47070  tmachlem-franscan  47960  uniimaelsetpreimafv  48479  iinfssc  50166  iinfsubc  50167  imaid  50263  uobrcl  50302  uobeq2  50510  thincciso4  50566  termcbas2  50591  termchom  50597  termcterm2  50623  euendfunc  50635  termcarweu  50637  diag1f1o  50643  diag2f1o  50646  termfucterm  50653  uobeqterm  50655