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  3523  dcun  3601  ifsbdc  3615  ifcldadc  3632  ifeq1dadc  3633  ifeq2dadc  3634  ifeqdadc  3635  ifbothdadc  3636  ifbothdc  3637  ifiddc  3638  eqifdc  3639  2if2dc  3642  ifordc  3644  exmid1dc  4284  exmidn0m  4285  exmidundif  4290  exmidundifim  4291  dcextest  4673  dcdifsnid  6658  pw2f1odclem  7003  fidceq  7039  fidifsnen  7040  fimax2gtrilemstep  7070  finexdc  7072  unfiexmid  7088  unsnfidcex  7090  unsnfidcel  7091  undifdcss  7093  prfidceq  7098  tpfidceq  7100  ssfirab  7106  fidcenumlemrks  7128  omp1eomlem  7269  difinfsnlem  7274  difinfsn  7275  ctssdc  7288  nnnninf  7301  nnnninfeq2  7304  nninfisol  7308  exmidomniim  7316  nninfwlpoimlemg  7350  exmidfodomrlemim  7387  netap  7448  2omotaplemap  7451  xaddcom  10065  xnegdi  10072  xpncan  10075  xleadd1a  10077  xsubge0  10085  exfzdc  10454  zsupcllemstep  10457  infssuzex  10461  flqeqceilz  10548  modifeq2int  10616  modfzo0difsn  10625  modsumfzodifsn  10626  iseqf1olemab  10732  iseqf1olemmo  10735  seq3f1olemstep  10744  seqf1oglem1  10749  fser0const  10765  bcval  10979  bccmpl  10984  bcval5  10993  bcpasc  10996  bccl  10997  hashfzp1  11054  ccatsymb  11145  fzowrddc  11187  swrd0g  11200  swrdsbslen  11206  swrdspsleq  11207  pfxclz  11219  pfxccatin12  11273  swrdccat  11275  pfxccat3a  11278  swrdccat3blem  11279  2zsupmax  11745  2zinfmin  11762  xrmaxifle  11765  xrmaxiflemab  11766  xrmaxiflemlub  11767  xrmaxiflemcom  11768  sumdc  11877  sumrbdclem  11896  fsum3cvg  11897  summodclem2a  11900  zsumdc  11903  isumss  11910  fisumss  11911  isumss2  11912  fsumadd  11925  sumsplitdc  11951  fsummulc2  11967  prodrbdclem  12090  fproddccvg  12091  zproddc  12098  prod1dc  12105  prodssdc  12108  fprodssdc  12109  fprodmul  12110  fprodsplitdc  12115  dvdsabseq  12366  bitsmod  12475  gcdval  12488  gcddvds  12492  gcdcl  12495  gcd0id  12508  gcdneg  12511  gcdaddm  12513  dfgcd3  12539  dfgcd2  12543  gcdmultiplez  12550  dvdssq  12560  dvdslcm  12599  lcmcl  12602  lcmneg  12604  lcmgcd  12608  lcmdvds  12609  lcmid  12610  mulgcddvds  12624  cncongr2  12634  prmind2  12650  rpexp  12683  pw2dvdslemn  12695  fermltl  12764  pclemdc  12819  pcxcl  12842  pcgcd  12860  pcmptcl  12873  pcmpt  12874  pcmpt2  12875  pcprod  12877  fldivp1  12879  1arith  12898  unennn  12976  ennnfonelemss  12989  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ctiunctlemudc  13016  bassetsnn  13097  gsumfzz  13536  gsumfzcl  13540  gsumfzreidx  13882  gsumfzsubmcl  13883  gsumfzmptfidmadd  13884  gsumfzmhm  13888  gsumfzfsum  14560  znf1o  14623  lgslem4  15690  lgsneg  15711  lgsmod  15713  lgsdilem  15714  lgsdir2  15720  lgsdir  15722  lgsdi  15724  lgsne0  15725  lgsdirnn0  15734  lgsdinn0  15735  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  lgsquadlem2  15765  lgsquad3  15771  2lgs  15791  sumdc2  16187  fidcen  16379  2omap  16388  nnsf  16401  nninfsellemsuc  16408  nninffeq  16416  apdifflemr  16445  nconstwlpolem  16463