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  2088  rabxmdc  3482  dcun  3560  ifsbdc  3573  ifcldadc  3590  ifeq1dadc  3591  ifeq2dadc  3592  ifbothdadc  3593  ifbothdc  3594  ifiddc  3595  eqifdc  3596  ifordc  3600  exmid1dc  4233  exmidn0m  4234  exmidundif  4239  exmidundifim  4240  dcextest  4617  dcdifsnid  6562  pw2f1odclem  6895  fidceq  6930  fidifsnen  6931  fimax2gtrilemstep  6961  finexdc  6963  unfiexmid  6979  unsnfidcex  6981  unsnfidcel  6982  undifdcss  6984  prfidceq  6989  tpfidceq  6991  ssfirab  6997  fidcenumlemrks  7019  omp1eomlem  7160  difinfsnlem  7165  difinfsn  7166  ctssdc  7179  nnnninf  7192  nnnninfeq2  7195  nninfisol  7199  exmidomniim  7207  nninfwlpoimlemg  7241  exmidfodomrlemim  7268  netap  7321  2omotaplemap  7324  xaddcom  9936  xnegdi  9943  xpncan  9946  xleadd1a  9948  xsubge0  9956  exfzdc  10316  zsupcllemstep  10319  infssuzex  10323  flqeqceilz  10410  modifeq2int  10478  modfzo0difsn  10487  modsumfzodifsn  10488  iseqf1olemab  10594  iseqf1olemmo  10597  seq3f1olemstep  10606  seqf1oglem1  10611  fser0const  10627  bcval  10841  bccmpl  10846  bcval5  10855  bcpasc  10858  bccl  10859  hashfzp1  10916  2zsupmax  11391  2zinfmin  11408  xrmaxifle  11411  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxiflemcom  11414  sumdc  11523  sumrbdclem  11542  fsum3cvg  11543  summodclem2a  11546  zsumdc  11549  isumss  11556  fisumss  11557  isumss2  11558  fsumadd  11571  sumsplitdc  11597  fsummulc2  11613  prodrbdclem  11736  fproddccvg  11737  zproddc  11744  prod1dc  11751  prodssdc  11754  fprodssdc  11755  fprodmul  11756  fprodsplitdc  11761  dvdsabseq  12012  gcdval  12126  gcddvds  12130  gcdcl  12133  gcd0id  12146  gcdneg  12149  gcdaddm  12151  dfgcd3  12177  dfgcd2  12181  gcdmultiplez  12188  dvdssq  12198  dvdslcm  12237  lcmcl  12240  lcmneg  12242  lcmgcd  12246  lcmdvds  12247  lcmid  12248  mulgcddvds  12262  cncongr2  12272  prmind2  12288  rpexp  12321  pw2dvdslemn  12333  fermltl  12402  pclemdc  12457  pcxcl  12480  pcgcd  12498  pcmptcl  12511  pcmpt  12512  pcmpt2  12513  pcprod  12515  fldivp1  12517  1arith  12536  unennn  12614  ennnfonelemss  12627  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ctiunctlemudc  12654  gsumfzz  13127  gsumfzcl  13131  gsumfzreidx  13467  gsumfzsubmcl  13468  gsumfzmptfidmadd  13469  gsumfzmhm  13473  gsumfzfsum  14144  znf1o  14207  lgslem4  15244  lgsneg  15265  lgsmod  15267  lgsdilem  15268  lgsdir2  15274  lgsdir  15276  lgsdi  15278  lgsne0  15279  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  lgsquadlem2  15319  lgsquad3  15325  2lgs  15345  sumdc2  15445  nnsf  15649  nninfsellemsuc  15656  nninffeq  15664  apdifflemr  15691  nconstwlpolem  15709