Theorem exmiddc 840

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 839	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2	1	biimpi 120	1 ⊢ (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 712  DECID wdc 838

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 839

This theorem is referenced by:  stdcndcOLD  850  modc  2101  rabxmdc  3503  dcun  3581  ifsbdc  3595  ifcldadc  3612  ifeq1dadc  3613  ifeq2dadc  3614  ifeqdadc  3615  ifbothdadc  3616  ifbothdc  3617  ifiddc  3618  eqifdc  3619  2if2dc  3622  ifordc  3624  exmid1dc  4263  exmidn0m  4264  exmidundif  4269  exmidundifim  4270  dcextest  4650  dcdifsnid  6620  pw2f1odclem  6963  fidceq  6999  fidifsnen  7000  fimax2gtrilemstep  7030  finexdc  7032  unfiexmid  7048  unsnfidcex  7050  unsnfidcel  7051  undifdcss  7053  prfidceq  7058  tpfidceq  7060  ssfirab  7066  fidcenumlemrks  7088  omp1eomlem  7229  difinfsnlem  7234  difinfsn  7235  ctssdc  7248  nnnninf  7261  nnnninfeq2  7264  nninfisol  7268  exmidomniim  7276  nninfwlpoimlemg  7310  exmidfodomrlemim  7347  netap  7408  2omotaplemap  7411  xaddcom  10025  xnegdi  10032  xpncan  10035  xleadd1a  10037  xsubge0  10045  exfzdc  10413  zsupcllemstep  10416  infssuzex  10420  flqeqceilz  10507  modifeq2int  10575  modfzo0difsn  10584  modsumfzodifsn  10585  iseqf1olemab  10691  iseqf1olemmo  10694  seq3f1olemstep  10703  seqf1oglem1  10708  fser0const  10724  bcval  10938  bccmpl  10943  bcval5  10952  bcpasc  10955  bccl  10956  hashfzp1  11013  ccatsymb  11103  fzowrddc  11145  swrd0g  11158  swrdsbslen  11164  swrdspsleq  11165  pfxclz  11177  pfxccatin12  11231  swrdccat  11233  pfxccat3a  11236  swrdccat3blem  11237  2zsupmax  11703  2zinfmin  11720  xrmaxifle  11723  xrmaxiflemab  11724  xrmaxiflemlub  11725  xrmaxiflemcom  11726  sumdc  11835  sumrbdclem  11854  fsum3cvg  11855  summodclem2a  11858  zsumdc  11861  isumss  11868  fisumss  11869  isumss2  11870  fsumadd  11883  sumsplitdc  11909  fsummulc2  11925  prodrbdclem  12048  fproddccvg  12049  zproddc  12056  prod1dc  12063  prodssdc  12066  fprodssdc  12067  fprodmul  12068  fprodsplitdc  12073  dvdsabseq  12324  bitsmod  12433  gcdval  12446  gcddvds  12450  gcdcl  12453  gcd0id  12466  gcdneg  12469  gcdaddm  12471  dfgcd3  12497  dfgcd2  12501  gcdmultiplez  12508  dvdssq  12518  dvdslcm  12557  lcmcl  12560  lcmneg  12562  lcmgcd  12566  lcmdvds  12567  lcmid  12568  mulgcddvds  12582  cncongr2  12592  prmind2  12608  rpexp  12641  pw2dvdslemn  12653  fermltl  12722  pclemdc  12777  pcxcl  12800  pcgcd  12818  pcmptcl  12831  pcmpt  12832  pcmpt2  12833  pcprod  12835  fldivp1  12837  1arith  12856  unennn  12934  ennnfonelemss  12947  ennnfonelemkh  12949  ennnfonelemhf1o  12950  ctiunctlemudc  12974  bassetsnn  13055  gsumfzz  13494  gsumfzcl  13498  gsumfzreidx  13840  gsumfzsubmcl  13841  gsumfzmptfidmadd  13842  gsumfzmhm  13846  gsumfzfsum  14517  znf1o  14580  lgslem4  15647  lgsneg  15668  lgsmod  15670  lgsdilem  15671  lgsdir2  15677  lgsdir  15679  lgsdi  15681  lgsne0  15682  lgsdirnn0  15691  lgsdinn0  15692  gausslemma2dlem1a  15702  gausslemma2dlem1f1o  15704  lgsquadlem2  15722  lgsquad3  15728  2lgs  15748  sumdc2  16073  2omap  16270  nnsf  16282  nninfsellemsuc  16289  nninffeq  16297  apdifflemr  16326  nconstwlpolem  16344