Theorem exmiddc 844

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 716  DECID wdc 842

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 843

This theorem is referenced by:  stdcndcOLD  854  dfifp2dc  990  ifpiddc  1000  modc  2126  rabxmdc  3542  dcun  3621  ifsbdc  3637  ifcldadc  3654  ifeq1dadc  3655  ifeq2dadc  3656  ifeqdadc  3657  ifbothdadc  3658  ifbothdc  3659  ifiddc  3660  eqifdc  3661  2if2dc  3664  ifordc  3666  exmid1dc  4315  exmidn0m  4316  exmidundif  4321  exmidundifim  4322  dcextest  4705  dcdifsnid  6739  pw2f1odclem  7089  fidceq  7126  fidifsnen  7127  fidcen  7158  fimax2gtrilemstep  7160  finexdc  7162  elssdc  7164  eqsndc  7165  unfiexmid  7180  unsnfidcex  7182  unsnfidcel  7183  undifdcss  7185  prfidceq  7190  tpfidceq  7192  ssfirab  7199  fidcenumlemrks  7225  2omap  7271  omp1eomlem  7387  difinfsnlem  7392  difinfsn  7393  ctssdc  7406  nnnninf  7419  nnnninfeq2  7422  nninfisol  7426  exmidomniim  7434  nninfwlpoimlemg  7468  exmidfodomrlemim  7506  netap  7573  2omotaplemap  7576  xaddcom  10200  xnegdi  10207  xpncan  10210  xleadd1a  10212  xsubge0  10220  exfzdc  10593  zsupcllemstep  10596  infssuzex  10600  flqeqceilz  10687  modifeq2int  10755  modfzo0difsn  10764  modsumfzodifsn  10765  iseqf1olemab  10871  iseqf1olemmo  10874  seq3f1olemstep  10883  seqf1oglem1  10888  fser0const  10904  bcval  11119  bccmpl  11124  bcval5  11133  bcpasc  11136  bccl  11137  hashfzp1  11197  hashfibc  11215  ccatsymb  11298  fzowrddc  11347  swrd0g  11360  swrdsbslen  11366  swrdspsleq  11367  pfxclz  11379  pfxccatin12  11433  swrdccat  11435  pfxccat3a  11438  swrdccat3blem  11439  2zsupmax  11919  2zinfmin  11936  xrmaxifle  11939  xrmaxiflemab  11940  xrmaxiflemlub  11941  xrmaxiflemcom  11942  sumdc  12051  sumrbdclem  12071  fsum3cvg  12072  summodclem2a  12075  zsumdc  12078  isumss  12085  fisumss  12086  isumss2  12087  fsumadd  12100  sumsplitdc  12126  fsummulc2  12142  prodrbdclem  12265  fproddccvg  12266  zproddc  12273  prod1dc  12280  prodssdc  12283  fprodssdc  12284  fprodmul  12285  fprodsplitdc  12290  dvdsabseq  12541  bitsmod  12650  gcdval  12663  gcddvds  12667  gcdcl  12670  gcd0id  12683  gcdneg  12686  gcdaddm  12688  dfgcd3  12714  dfgcd2  12718  gcdmultiplez  12725  dvdssq  12735  dvdslcm  12774  lcmcl  12777  lcmneg  12779  lcmgcd  12783  lcmdvds  12784  lcmid  12785  mulgcddvds  12799  cncongr2  12809  prmind2  12825  rpexp  12858  pw2dvdslemn  12870  fermltl  12939  pclemdc  12994  pcxcl  13017  pcgcd  13035  pcmptcl  13048  pcmpt  13049  pcmpt2  13050  pcprod  13052  fldivp1  13054  1arith  13073  unennn  13169  ennnfonelemss  13182  ennnfonelemkh  13184  ennnfonelemhf1o  13185  ctiunctlemudc  13209  bassetsnn  13290  gsumfzz  13729  gsumfzcl  13733  gsumfzreidx  14075  gsumfzsubmcl  14076  gsumfzmptfidmadd  14077  gsumfzmhm  14081  gsumfzfsum  14785  znf1o  14848  lgslem4  15925  lgsneg  15946  lgsmod  15948  lgsdilem  15949  lgsdir2  15955  lgsdir  15957  lgsdi  15959  lgsne0  15960  lgsdirnn0  15969  lgsdinn0  15970  gausslemma2dlem1a  15980  gausslemma2dlem1f1o  15982  lgsquadlem2  16000  lgsquad3  16006  2lgs  16026  umgrclwwlkge2  16446  eupth2lem3lem4fi  16517  eupth2lem3lem7fi  16518  sumdc2  16620  nnsf  16832  nninfsellemsuc  16839  nninffeq  16847  apdifflemr  16880  trimul0or  16894  nconstwlpolem  16900  gsumgfsum  16915