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

Theorem exmiddc 780
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  ph  ->  (
ph  \/  -.  ph )
)

Proof of Theorem exmiddc
StepHypRef Expression
1 df-dc 779 . 2  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
21biimpi 118 1  |-  (DECID  ph  ->  (
ph  \/  -.  ph )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 662  DECID wdc 778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-dc 779
This theorem is referenced by:  stabtestimpdc  860  modc  1988  rabxmdc  3303  ifsbdc  3391  ifcldadc  3406  ifeq1dadc  3407  ifbothdadc  3408  ifbothdc  3409  ifiddc  3410  eqifdc  3411  exmidundif  4011  dcextest  4371  dcdifsnid  6219  fidceq  6539  fidifsnen  6540  fimax2gtrilemstep  6570  finexdc  6572  unfiexmid  6582  unsnfidcex  6584  unsnfidcel  6585  undifdcss  6587  ssfirab  6596  exmidomniim  6744  nnnninf  6753  exmidfodomrlemim  6774  exfzdc  9582  flqeqceilz  9656  modifeq2int  9724  modfzo0difsn  9733  modsumfzodifsn  9734  iseqf1olemab  9842  iseqf1olemmo  9845  iseqf1olemstep  9854  fser0const  9871  bcval  10075  bccmpl  10080  ibcval5  10089  bcpasc  10092  bccl  10093  hashfzp1  10150  sumdc  10661  isumrblem  10679  fisumcvg  10680  isummolem2a  10684  zisum  10687  isumss  10693  fisumss  10694  isumss2  10695  fsumadd  10707  dvdsabseq  10773  zsupcllemstep  10866  infssuzex  10870  gcdval  10876  gcddvds  10880  gcdcl  10883  gcd0id  10895  gcdneg  10898  gcdaddm  10900  dfgcd3  10924  dfgcd2  10928  gcdmultiplez  10935  dvdssq  10945  dvdslcm  10976  lcmcl  10979  lcmneg  10981  lcmgcd  10985  lcmdvds  10986  lcmid  10987  mulgcddvds  11001  cncongr2  11011  prmind2  11027  rpexp  11057  pw2dvdslemn  11068  unennn  11135  sumdc2  11187  nnsf  11383  nninfsellemsuc  11392
  Copyright terms: Public domain W3C validator