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  2123  rabxmdc  3528  dcun  3606  ifsbdc  3622  ifcldadc  3639  ifeq1dadc  3640  ifeq2dadc  3641  ifeqdadc  3642  ifbothdadc  3643  ifbothdc  3644  ifiddc  3645  eqifdc  3646  2if2dc  3649  ifordc  3651  exmid1dc  4296  exmidn0m  4297  exmidundif  4302  exmidundifim  4303  dcextest  4685  dcdifsnid  6715  pw2f1odclem  7063  fidceq  7099  fidifsnen  7100  fidcen  7131  fimax2gtrilemstep  7133  finexdc  7135  elssdc  7137  eqsndc  7138  unfiexmid  7153  unsnfidcex  7155  unsnfidcel  7156  undifdcss  7158  prfidceq  7163  tpfidceq  7165  ssfirab  7172  fidcenumlemrks  7195  omp1eomlem  7336  difinfsnlem  7341  difinfsn  7342  ctssdc  7355  nnnninf  7368  nnnninfeq2  7371  nninfisol  7375  exmidomniim  7383  nninfwlpoimlemg  7417  exmidfodomrlemim  7455  netap  7516  2omotaplemap  7519  xaddcom  10140  xnegdi  10147  xpncan  10150  xleadd1a  10152  xsubge0  10160  exfzdc  10532  zsupcllemstep  10535  infssuzex  10539  flqeqceilz  10626  modifeq2int  10694  modfzo0difsn  10703  modsumfzodifsn  10704  iseqf1olemab  10810  iseqf1olemmo  10813  seq3f1olemstep  10822  seqf1oglem1  10827  fser0const  10843  bcval  11057  bccmpl  11062  bcval5  11071  bcpasc  11074  bccl  11075  hashfzp1  11134  ccatsymb  11228  fzowrddc  11277  swrd0g  11290  swrdsbslen  11296  swrdspsleq  11297  pfxclz  11309  pfxccatin12  11363  swrdccat  11365  pfxccat3a  11368  swrdccat3blem  11369  2zsupmax  11849  2zinfmin  11866  xrmaxifle  11869  xrmaxiflemab  11870  xrmaxiflemlub  11871  xrmaxiflemcom  11872  sumdc  11981  sumrbdclem  12001  fsum3cvg  12002  summodclem2a  12005  zsumdc  12008  isumss  12015  fisumss  12016  isumss2  12017  fsumadd  12030  sumsplitdc  12056  fsummulc2  12072  prodrbdclem  12195  fproddccvg  12196  zproddc  12203  prod1dc  12210  prodssdc  12213  fprodssdc  12214  fprodmul  12215  fprodsplitdc  12220  dvdsabseq  12471  bitsmod  12580  gcdval  12593  gcddvds  12597  gcdcl  12600  gcd0id  12613  gcdneg  12616  gcdaddm  12618  dfgcd3  12644  dfgcd2  12648  gcdmultiplez  12655  dvdssq  12665  dvdslcm  12704  lcmcl  12707  lcmneg  12709  lcmgcd  12713  lcmdvds  12714  lcmid  12715  mulgcddvds  12729  cncongr2  12739  prmind2  12755  rpexp  12788  pw2dvdslemn  12800  fermltl  12869  pclemdc  12924  pcxcl  12947  pcgcd  12965  pcmptcl  12978  pcmpt  12979  pcmpt2  12980  pcprod  12982  fldivp1  12984  1arith  13003  unennn  13081  ennnfonelemss  13094  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ctiunctlemudc  13121  bassetsnn  13202  gsumfzz  13641  gsumfzcl  13645  gsumfzreidx  13987  gsumfzsubmcl  13988  gsumfzmptfidmadd  13989  gsumfzmhm  13993  gsumfzfsum  14667  znf1o  14730  lgslem4  15805  lgsneg  15826  lgsmod  15828  lgsdilem  15829  lgsdir2  15835  lgsdir  15837  lgsdi  15839  lgsne0  15840  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem1a  15860  gausslemma2dlem1f1o  15862  lgsquadlem2  15880  lgsquad3  15886  2lgs  15906  umgrclwwlkge2  16326  eupth2lem3lem4fi  16397  eupth2lem3lem7fi  16398  sumdc2  16500  2omap  16698  nnsf  16714  nninfsellemsuc  16721  nninffeq  16729  apdifflemr  16762  nconstwlpolem  16781  gsumgfsum  16796