Theorem exmiddc 826

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 698  DECID wdc 824

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 825

This theorem is referenced by:  stdcndcOLD  836  modc  2057  rabxmdc  3440  dcun  3519  ifsbdc  3532  ifcldadc  3549  ifeq1dadc  3550  ifbothdadc  3551  ifbothdc  3552  ifiddc  3553  eqifdc  3554  exmid1dc  4179  exmidn0m  4180  exmidundif  4185  exmidundifim  4186  dcextest  4558  dcdifsnid  6472  fidceq  6835  fidifsnen  6836  fimax2gtrilemstep  6866  finexdc  6868  unfiexmid  6883  unsnfidcex  6885  unsnfidcel  6886  undifdcss  6888  ssfirab  6899  fidcenumlemrks  6918  omp1eomlem  7059  difinfsnlem  7064  difinfsn  7065  ctssdc  7078  nnnninf  7090  nnnninfeq2  7093  nninfisol  7097  exmidomniim  7105  exmidfodomrlemim  7157  xaddcom  9797  xnegdi  9804  xpncan  9807  xleadd1a  9809  xsubge0  9817  exfzdc  10175  flqeqceilz  10253  modifeq2int  10321  modfzo0difsn  10330  modsumfzodifsn  10331  iseqf1olemab  10424  iseqf1olemmo  10427  seq3f1olemstep  10436  fser0const  10451  bcval  10662  bccmpl  10667  bcval5  10676  bcpasc  10679  bccl  10680  hashfzp1  10737  2zsupmax  11167  2zinfmin  11184  xrmaxifle  11187  xrmaxiflemab  11188  xrmaxiflemlub  11189  xrmaxiflemcom  11190  sumdc  11299  sumrbdclem  11318  fsum3cvg  11319  summodclem2a  11322  zsumdc  11325  isumss  11332  fisumss  11333  isumss2  11334  fsumadd  11347  sumsplitdc  11373  fsummulc2  11389  prodrbdclem  11512  fproddccvg  11513  zproddc  11520  prod1dc  11527  prodssdc  11530  fprodssdc  11531  fprodmul  11532  fprodsplitdc  11537  dvdsabseq  11785  zsupcllemstep  11878  infssuzex  11882  gcdval  11892  gcddvds  11896  gcdcl  11899  gcd0id  11912  gcdneg  11915  gcdaddm  11917  dfgcd3  11943  dfgcd2  11947  gcdmultiplez  11954  dvdssq  11964  dvdslcm  12001  lcmcl  12004  lcmneg  12006  lcmgcd  12010  lcmdvds  12011  lcmid  12012  mulgcddvds  12026  cncongr2  12036  prmind2  12052  rpexp  12085  pw2dvdslemn  12097  fermltl  12166  pclemdc  12220  pcxcl  12243  pcgcd  12260  pcmptcl  12272  pcmpt  12273  pcmpt2  12274  pcprod  12276  fldivp1  12278  1arith  12297  unennn  12330  ennnfonelemss  12343  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ctiunctlemudc  12370  lgslem4  13544  lgsneg  13565  lgsmod  13567  lgsdilem  13568  lgsdir2  13574  lgsdir  13576  lgsdi  13578  lgsne0  13579  lgsdirnn0  13588  lgsdinn0  13589  sumdc2  13680  nnsf  13885  nninfsellemsuc  13892  nninffeq  13900  apdifflemr  13926  nconstwlpolem  13943