Theorem exmiddc 837

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 836	. 2 |- (DECID ph <-> ( ph \/ -. ph ) )
2	1	biimpi 120	1 |- (DECID ph -> ( ph \/ -. ph ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 709  DECID wdc 835

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 836

This theorem is referenced by:  stdcndcOLD  847  modc  2085  rabxmdc  3479  dcun  3557  ifsbdc  3570  ifcldadc  3587  ifeq1dadc  3588  ifeq2dadc  3589  ifbothdadc  3590  ifbothdc  3591  ifiddc  3592  eqifdc  3593  ifordc  3597  exmid1dc  4230  exmidn0m  4231  exmidundif  4236  exmidundifim  4237  dcextest  4614  dcdifsnid  6559  pw2f1odclem  6892  fidceq  6927  fidifsnen  6928  fimax2gtrilemstep  6958  finexdc  6960  unfiexmid  6976  unsnfidcex  6978  unsnfidcel  6979  undifdcss  6981  ssfirab  6992  fidcenumlemrks  7014  omp1eomlem  7155  difinfsnlem  7160  difinfsn  7161  ctssdc  7174  nnnninf  7187  nnnninfeq2  7190  nninfisol  7194  exmidomniim  7202  nninfwlpoimlemg  7236  exmidfodomrlemim  7263  netap  7316  2omotaplemap  7319  xaddcom  9930  xnegdi  9937  xpncan  9940  xleadd1a  9942  xsubge0  9950  exfzdc  10310  flqeqceilz  10392  modifeq2int  10460  modfzo0difsn  10469  modsumfzodifsn  10470  iseqf1olemab  10576  iseqf1olemmo  10579  seq3f1olemstep  10588  seqf1oglem1  10593  fser0const  10609  bcval  10823  bccmpl  10828  bcval5  10837  bcpasc  10840  bccl  10841  hashfzp1  10898  2zsupmax  11372  2zinfmin  11389  xrmaxifle  11392  xrmaxiflemab  11393  xrmaxiflemlub  11394  xrmaxiflemcom  11395  sumdc  11504  sumrbdclem  11523  fsum3cvg  11524  summodclem2a  11527  zsumdc  11530  isumss  11537  fisumss  11538  isumss2  11539  fsumadd  11552  sumsplitdc  11578  fsummulc2  11594  prodrbdclem  11717  fproddccvg  11718  zproddc  11725  prod1dc  11732  prodssdc  11735  fprodssdc  11736  fprodmul  11737  fprodsplitdc  11742  dvdsabseq  11992  zsupcllemstep  12085  infssuzex  12089  gcdval  12099  gcddvds  12103  gcdcl  12106  gcd0id  12119  gcdneg  12122  gcdaddm  12124  dfgcd3  12150  dfgcd2  12154  gcdmultiplez  12161  dvdssq  12171  dvdslcm  12210  lcmcl  12213  lcmneg  12215  lcmgcd  12219  lcmdvds  12220  lcmid  12221  mulgcddvds  12235  cncongr2  12245  prmind2  12261  rpexp  12294  pw2dvdslemn  12306  fermltl  12375  pclemdc  12429  pcxcl  12452  pcgcd  12470  pcmptcl  12483  pcmpt  12484  pcmpt2  12485  pcprod  12487  fldivp1  12489  1arith  12508  unennn  12557  ennnfonelemss  12570  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ctiunctlemudc  12597  gsumfzz  13070  gsumfzcl  13074  gsumfzreidx  13410  gsumfzsubmcl  13411  gsumfzmptfidmadd  13412  gsumfzmhm  13416  gsumfzfsum  14087  znf1o  14150  lgslem4  15160  lgsneg  15181  lgsmod  15183  lgsdilem  15184  lgsdir2  15190  lgsdir  15192  lgsdi  15194  lgsne0  15195  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  lgsquadlem2  15235  lgsquad3  15241  2lgs  15261  sumdc2  15361  nnsf  15565  nninfsellemsuc  15572  nninffeq  15580  apdifflemr  15607  nconstwlpolem  15625