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

Theorem exmiddc 806
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 805 . 2  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
21biimpi 119 1  |-  (DECID  ph  ->  (
ph  \/  -.  ph )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 682  DECID wdc 804
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 805
This theorem is referenced by:  stdcndcOLD  816  modc  2020  rabxmdc  3364  dcun  3443  ifsbdc  3456  ifcldadc  3471  ifeq1dadc  3472  ifbothdadc  3473  ifbothdc  3474  ifiddc  3475  eqifdc  3476  exmid1dc  4093  exmidn0m  4094  exmidundif  4099  exmidundifim  4100  dcextest  4465  dcdifsnid  6368  fidceq  6731  fidifsnen  6732  fimax2gtrilemstep  6762  finexdc  6764  unfiexmid  6774  unsnfidcex  6776  unsnfidcel  6777  undifdcss  6779  ssfirab  6790  fidcenumlemrks  6809  omp1eomlem  6947  difinfsnlem  6952  difinfsn  6953  ctssdc  6966  exmidomniim  6981  nnnninf  6991  exmidfodomrlemim  7025  xaddcom  9599  xnegdi  9606  xpncan  9609  xleadd1a  9611  xsubge0  9619  exfzdc  9972  flqeqceilz  10046  modifeq2int  10114  modfzo0difsn  10123  modsumfzodifsn  10124  iseqf1olemab  10217  iseqf1olemmo  10220  seq3f1olemstep  10229  fser0const  10244  bcval  10450  bccmpl  10455  bcval5  10464  bcpasc  10467  bccl  10468  hashfzp1  10525  2zsupmax  10952  xrmaxifle  10970  xrmaxiflemab  10971  xrmaxiflemlub  10972  xrmaxiflemcom  10973  sumdc  11082  sumrbdclem  11100  fsum3cvg  11101  summodclem2a  11105  zsumdc  11108  isumss  11115  fisumss  11116  isumss2  11117  fsumadd  11130  sumsplitdc  11156  fsummulc2  11172  dvdsabseq  11457  zsupcllemstep  11550  infssuzex  11554  gcdval  11560  gcddvds  11564  gcdcl  11567  gcd0id  11579  gcdneg  11582  gcdaddm  11584  dfgcd3  11610  dfgcd2  11614  gcdmultiplez  11621  dvdssq  11631  dvdslcm  11662  lcmcl  11665  lcmneg  11667  lcmgcd  11671  lcmdvds  11672  lcmid  11673  mulgcddvds  11687  cncongr2  11697  prmind2  11713  rpexp  11743  pw2dvdslemn  11754  unennn  11821  ennnfonelemss  11834  ennnfonelemkh  11836  ennnfonelemhf1o  11837  ctiunctlemudc  11861  sumdc2  12902  nnsf  13095  nninfsellemsuc  13104  nninffeq  13112
  Copyright terms: Public domain W3C validator