Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  exmiddc Unicode version

Theorem exmiddc 822
 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
StepHypRef Expression
1 df-dc 821 . 2 DECID
21biimpi 119 1 DECID
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wo 698  DECID wdc 820 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105 This theorem depends on definitions:  df-bi 116  df-dc 821 This theorem is referenced by:  stdcndcOLD  832  modc  2033  rabxmdc  3401  dcun  3480  ifsbdc  3493  ifcldadc  3508  ifeq1dadc  3509  ifbothdadc  3510  ifbothdc  3511  ifiddc  3512  eqifdc  3513  exmid1dc  4134  exmidn0m  4135  exmidundif  4140  exmidundifim  4141  dcextest  4506  dcdifsnid  6412  fidceq  6775  fidifsnen  6776  fimax2gtrilemstep  6806  finexdc  6808  unfiexmid  6823  unsnfidcex  6825  unsnfidcel  6826  undifdcss  6828  ssfirab  6839  fidcenumlemrks  6858  omp1eomlem  6996  difinfsnlem  7001  difinfsn  7002  ctssdc  7015  nnnninf  7025  exmidomniim  7034  exmidfodomrlemim  7086  xaddcom  9703  xnegdi  9710  xpncan  9713  xleadd1a  9715  xsubge0  9723  exfzdc  10077  flqeqceilz  10151  modifeq2int  10219  modfzo0difsn  10228  modsumfzodifsn  10229  iseqf1olemab  10322  iseqf1olemmo  10325  seq3f1olemstep  10334  fser0const  10349  bcval  10556  bccmpl  10561  bcval5  10570  bcpasc  10573  bccl  10574  hashfzp1  10631  2zsupmax  11058  xrmaxifle  11076  xrmaxiflemab  11077  xrmaxiflemlub  11078  xrmaxiflemcom  11079  sumdc  11188  sumrbdclem  11207  fsum3cvg  11208  summodclem2a  11211  zsumdc  11214  isumss  11221  fisumss  11222  isumss2  11223  fsumadd  11236  sumsplitdc  11262  fsummulc2  11278  prodrbdclem  11401  fproddccvg  11402  zproddc  11409  prod1dc  11416  prodssdc  11419  fprodssdc  11420  dvdsabseq  11617  zsupcllemstep  11710  infssuzex  11714  gcdval  11720  gcddvds  11724  gcdcl  11727  gcd0id  11739  gcdneg  11742  gcdaddm  11744  dfgcd3  11770  dfgcd2  11774  gcdmultiplez  11781  dvdssq  11791  dvdslcm  11822  lcmcl  11825  lcmneg  11827  lcmgcd  11831  lcmdvds  11832  lcmid  11833  mulgcddvds  11847  cncongr2  11857  prmind2  11873  rpexp  11903  pw2dvdslemn  11915  unennn  11982  ennnfonelemss  11995  ennnfonelemkh  11997  ennnfonelemhf1o  11998  ctiunctlemudc  12022  sumdc2  13216  nnsf  13418  nninfsellemsuc  13427  nninffeq  13435  apdifflemr  13461  nconstwlpolem  13478
 Copyright terms: Public domain W3C validator