Theorem exmiddc 836

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

Step	Hyp	Ref	Expression
1		df-dc 835	. 2 |- (DECID ph <-> ( ph \/ -. ph ) )
2	1	biimpi 120	1 |- (DECID ph -> ( ph \/ -. ph ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 708  DECID wdc 834

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 835

This theorem is referenced by:  stdcndcOLD  846  modc  2069  rabxmdc  3456  dcun  3535  ifsbdc  3548  ifcldadc  3565  ifeq1dadc  3566  ifeq2dadc  3567  ifbothdadc  3568  ifbothdc  3569  ifiddc  3570  eqifdc  3571  ifordc  3575  exmid1dc  4202  exmidn0m  4203  exmidundif  4208  exmidundifim  4209  dcextest  4582  dcdifsnid  6507  fidceq  6871  fidifsnen  6872  fimax2gtrilemstep  6902  finexdc  6904  unfiexmid  6919  unsnfidcex  6921  unsnfidcel  6922  undifdcss  6924  ssfirab  6935  fidcenumlemrks  6954  omp1eomlem  7095  difinfsnlem  7100  difinfsn  7101  ctssdc  7114  nnnninf  7126  nnnninfeq2  7129  nninfisol  7133  exmidomniim  7141  nninfwlpoimlemg  7175  exmidfodomrlemim  7202  netap  7255  2omotaplemap  7258  xaddcom  9863  xnegdi  9870  xpncan  9873  xleadd1a  9875  xsubge0  9883  exfzdc  10242  flqeqceilz  10320  modifeq2int  10388  modfzo0difsn  10397  modsumfzodifsn  10398  iseqf1olemab  10491  iseqf1olemmo  10494  seq3f1olemstep  10503  fser0const  10518  bcval  10731  bccmpl  10736  bcval5  10745  bcpasc  10748  bccl  10749  hashfzp1  10806  2zsupmax  11236  2zinfmin  11253  xrmaxifle  11256  xrmaxiflemab  11257  xrmaxiflemlub  11258  xrmaxiflemcom  11259  sumdc  11368  sumrbdclem  11387  fsum3cvg  11388  summodclem2a  11391  zsumdc  11394  isumss  11401  fisumss  11402  isumss2  11403  fsumadd  11416  sumsplitdc  11442  fsummulc2  11458  prodrbdclem  11581  fproddccvg  11582  zproddc  11589  prod1dc  11596  prodssdc  11599  fprodssdc  11600  fprodmul  11601  fprodsplitdc  11606  dvdsabseq  11855  zsupcllemstep  11948  infssuzex  11952  gcdval  11962  gcddvds  11966  gcdcl  11969  gcd0id  11982  gcdneg  11985  gcdaddm  11987  dfgcd3  12013  dfgcd2  12017  gcdmultiplez  12024  dvdssq  12034  dvdslcm  12071  lcmcl  12074  lcmneg  12076  lcmgcd  12080  lcmdvds  12081  lcmid  12082  mulgcddvds  12096  cncongr2  12106  prmind2  12122  rpexp  12155  pw2dvdslemn  12167  fermltl  12236  pclemdc  12290  pcxcl  12313  pcgcd  12330  pcmptcl  12342  pcmpt  12343  pcmpt2  12344  pcprod  12346  fldivp1  12348  1arith  12367  unennn  12400  ennnfonelemss  12413  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ctiunctlemudc  12440  lgslem4  14443  lgsneg  14464  lgsmod  14466  lgsdilem  14467  lgsdir2  14473  lgsdir  14475  lgsdi  14477  lgsne0  14478  lgsdirnn0  14487  lgsdinn0  14488  sumdc2  14590  nnsf  14793  nninfsellemsuc  14800  nninffeq  14808  apdifflemr  14834  nconstwlpolem  14852