Theorem exmiddc 844

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 716  DECID wdc 842

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 843

This theorem is referenced by:  stdcndcOLD  854  dfifp2dc  990  ifpiddc  1000  modc  2124  rabxmdc  3540  dcun  3619  ifsbdc  3635  ifcldadc  3652  ifeq1dadc  3653  ifeq2dadc  3654  ifeqdadc  3655  ifbothdadc  3656  ifbothdc  3657  ifiddc  3658  eqifdc  3659  2if2dc  3662  ifordc  3664  exmid1dc  4313  exmidn0m  4314  exmidundif  4319  exmidundifim  4320  dcextest  4703  dcdifsnid  6737  pw2f1odclem  7087  fidceq  7124  fidifsnen  7125  fidcen  7156  fimax2gtrilemstep  7158  finexdc  7160  elssdc  7162  eqsndc  7163  unfiexmid  7178  unsnfidcex  7180  unsnfidcel  7181  undifdcss  7183  prfidceq  7188  tpfidceq  7190  ssfirab  7197  fidcenumlemrks  7223  2omap  7269  omp1eomlem  7385  difinfsnlem  7390  difinfsn  7391  ctssdc  7404  nnnninf  7417  nnnninfeq2  7420  nninfisol  7424  exmidomniim  7432  nninfwlpoimlemg  7466  exmidfodomrlemim  7504  netap  7568  2omotaplemap  7571  xaddcom  10194  xnegdi  10201  xpncan  10204  xleadd1a  10206  xsubge0  10214  exfzdc  10586  zsupcllemstep  10589  infssuzex  10593  flqeqceilz  10680  modifeq2int  10748  modfzo0difsn  10757  modsumfzodifsn  10758  iseqf1olemab  10864  iseqf1olemmo  10867  seq3f1olemstep  10876  seqf1oglem1  10881  fser0const  10897  bcval  11111  bccmpl  11116  bcval5  11125  bcpasc  11128  bccl  11129  hashfzp1  11189  hashfibc  11207  ccatsymb  11290  fzowrddc  11339  swrd0g  11352  swrdsbslen  11358  swrdspsleq  11359  pfxclz  11371  pfxccatin12  11425  swrdccat  11427  pfxccat3a  11430  swrdccat3blem  11431  2zsupmax  11911  2zinfmin  11928  xrmaxifle  11931  xrmaxiflemab  11932  xrmaxiflemlub  11933  xrmaxiflemcom  11934  sumdc  12043  sumrbdclem  12063  fsum3cvg  12064  summodclem2a  12067  zsumdc  12070  isumss  12077  fisumss  12078  isumss2  12079  fsumadd  12092  sumsplitdc  12118  fsummulc2  12134  prodrbdclem  12257  fproddccvg  12258  zproddc  12265  prod1dc  12272  prodssdc  12275  fprodssdc  12276  fprodmul  12277  fprodsplitdc  12282  dvdsabseq  12533  bitsmod  12642  gcdval  12655  gcddvds  12659  gcdcl  12662  gcd0id  12675  gcdneg  12678  gcdaddm  12680  dfgcd3  12706  dfgcd2  12710  gcdmultiplez  12717  dvdssq  12727  dvdslcm  12766  lcmcl  12769  lcmneg  12771  lcmgcd  12775  lcmdvds  12776  lcmid  12777  mulgcddvds  12791  cncongr2  12801  prmind2  12817  rpexp  12850  pw2dvdslemn  12862  fermltl  12931  pclemdc  12986  pcxcl  13009  pcgcd  13027  pcmptcl  13040  pcmpt  13041  pcmpt2  13042  pcprod  13044  fldivp1  13046  1arith  13065  unennn  13148  ennnfonelemss  13161  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ctiunctlemudc  13188  bassetsnn  13269  gsumfzz  13708  gsumfzcl  13712  gsumfzreidx  14054  gsumfzsubmcl  14055  gsumfzmptfidmadd  14056  gsumfzmhm  14060  gsumfzfsum  14736  znf1o  14799  lgslem4  15876  lgsneg  15897  lgsmod  15899  lgsdilem  15900  lgsdir2  15906  lgsdir  15908  lgsdi  15910  lgsne0  15911  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  lgsquadlem2  15951  lgsquad3  15957  2lgs  15977  umgrclwwlkge2  16397  eupth2lem3lem4fi  16468  eupth2lem3lem7fi  16469  sumdc2  16571  nnsf  16783  nninfsellemsuc  16790  nninffeq  16798  apdifflemr  16831  trimul0or  16845  nconstwlpolem  16851  gsumgfsum  16866