Theorem exmiddc 841

Description: Law of excluded middle, for a decidable proposition. The law of the excluded middle is also called the principle of tertium non datur. Theorem *2.11 of [WhiteheadRussell] p. 101. It says that something is either true or not true; there are no in-between values of truth. The key way in which intuitionistic logic differs from classical logic is that intuitionistic logic says that excluded middle only holds for some propositions, and classical logic says that it holds for all propositions. (Contributed by Jim Kingdon, 12-May-2018.)

Assertion

Ref	Expression
exmiddc	⊢ (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑))

Proof of Theorem exmiddc

Step	Hyp	Ref	Expression
1		df-dc 840	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2	1	biimpi 120	1 ⊢ (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 713  DECID wdc 839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-dc 840

This theorem is referenced by:  stdcndcOLD  851  dfifp2dc  987  ifpiddc  997  modc  2121  rabxmdc  3524  dcun  3602  ifsbdc  3616  ifcldadc  3633  ifeq1dadc  3634  ifeq2dadc  3635  ifeqdadc  3636  ifbothdadc  3637  ifbothdc  3638  ifiddc  3639  eqifdc  3640  2if2dc  3643  ifordc  3645  exmid1dc  4288  exmidn0m  4289  exmidundif  4294  exmidundifim  4295  dcextest  4677  dcdifsnid  6667  pw2f1odclem  7015  fidceq  7051  fidifsnen  7052  fidcen  7083  fimax2gtrilemstep  7085  finexdc  7087  elssdc  7089  eqsndc  7090  unfiexmid  7105  unsnfidcex  7107  unsnfidcel  7108  undifdcss  7110  prfidceq  7115  tpfidceq  7117  ssfirab  7123  fidcenumlemrks  7146  omp1eomlem  7287  difinfsnlem  7292  difinfsn  7293  ctssdc  7306  nnnninf  7319  nnnninfeq2  7322  nninfisol  7326  exmidomniim  7334  nninfwlpoimlemg  7368  exmidfodomrlemim  7405  netap  7466  2omotaplemap  7469  xaddcom  10089  xnegdi  10096  xpncan  10099  xleadd1a  10101  xsubge0  10109  exfzdc  10479  zsupcllemstep  10482  infssuzex  10486  flqeqceilz  10573  modifeq2int  10641  modfzo0difsn  10650  modsumfzodifsn  10651  iseqf1olemab  10757  iseqf1olemmo  10760  seq3f1olemstep  10769  seqf1oglem1  10774  fser0const  10790  bcval  11004  bccmpl  11009  bcval5  11018  bcpasc  11021  bccl  11022  hashfzp1  11081  ccatsymb  11172  fzowrddc  11221  swrd0g  11234  swrdsbslen  11240  swrdspsleq  11241  pfxclz  11253  pfxccatin12  11307  swrdccat  11309  pfxccat3a  11312  swrdccat3blem  11313  2zsupmax  11780  2zinfmin  11797  xrmaxifle  11800  xrmaxiflemab  11801  xrmaxiflemlub  11802  xrmaxiflemcom  11803  sumdc  11912  sumrbdclem  11931  fsum3cvg  11932  summodclem2a  11935  zsumdc  11938  isumss  11945  fisumss  11946  isumss2  11947  fsumadd  11960  sumsplitdc  11986  fsummulc2  12002  prodrbdclem  12125  fproddccvg  12126  zproddc  12133  prod1dc  12140  prodssdc  12143  fprodssdc  12144  fprodmul  12145  fprodsplitdc  12150  dvdsabseq  12401  bitsmod  12510  gcdval  12523  gcddvds  12527  gcdcl  12530  gcd0id  12543  gcdneg  12546  gcdaddm  12548  dfgcd3  12574  dfgcd2  12578  gcdmultiplez  12585  dvdssq  12595  dvdslcm  12634  lcmcl  12637  lcmneg  12639  lcmgcd  12643  lcmdvds  12644  lcmid  12645  mulgcddvds  12659  cncongr2  12669  prmind2  12685  rpexp  12718  pw2dvdslemn  12730  fermltl  12799  pclemdc  12854  pcxcl  12877  pcgcd  12895  pcmptcl  12908  pcmpt  12909  pcmpt2  12910  pcprod  12912  fldivp1  12914  1arith  12933  unennn  13011  ennnfonelemss  13024  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ctiunctlemudc  13051  bassetsnn  13132  gsumfzz  13571  gsumfzcl  13575  gsumfzreidx  13917  gsumfzsubmcl  13918  gsumfzmptfidmadd  13919  gsumfzmhm  13923  gsumfzfsum  14595  znf1o  14658  lgslem4  15725  lgsneg  15746  lgsmod  15748  lgsdilem  15749  lgsdir2  15755  lgsdir  15757  lgsdi  15759  lgsne0  15760  lgsdirnn0  15769  lgsdinn0  15770  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  lgsquadlem2  15800  lgsquad3  15806  2lgs  15826  umgrclwwlkge2  16211  sumdc2  16345  2omap  16544  nnsf  16557  nninfsellemsuc  16564  nninffeq  16572  apdifflemr  16601  nconstwlpolem  16619  gsumgfsum  16634