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  2096  rabxmdc  3491  dcun  3569  ifsbdc  3582  ifcldadc  3599  ifeq1dadc  3600  ifeq2dadc  3601  ifeqdadc  3602  ifbothdadc  3603  ifbothdc  3604  ifiddc  3605  eqifdc  3606  ifordc  3610  exmid1dc  4243  exmidn0m  4244  exmidundif  4249  exmidundifim  4250  dcextest  4628  dcdifsnid  6589  pw2f1odclem  6930  fidceq  6965  fidifsnen  6966  fimax2gtrilemstep  6996  finexdc  6998  unfiexmid  7014  unsnfidcex  7016  unsnfidcel  7017  undifdcss  7019  prfidceq  7024  tpfidceq  7026  ssfirab  7032  fidcenumlemrks  7054  omp1eomlem  7195  difinfsnlem  7200  difinfsn  7201  ctssdc  7214  nnnninf  7227  nnnninfeq2  7230  nninfisol  7234  exmidomniim  7242  nninfwlpoimlemg  7276  exmidfodomrlemim  7308  netap  7365  2omotaplemap  7368  xaddcom  9982  xnegdi  9989  xpncan  9992  xleadd1a  9994  xsubge0  10002  exfzdc  10367  zsupcllemstep  10370  infssuzex  10374  flqeqceilz  10461  modifeq2int  10529  modfzo0difsn  10538  modsumfzodifsn  10539  iseqf1olemab  10645  iseqf1olemmo  10648  seq3f1olemstep  10657  seqf1oglem1  10662  fser0const  10678  bcval  10892  bccmpl  10897  bcval5  10906  bcpasc  10909  bccl  10910  hashfzp1  10967  ccatsymb  11056  2zsupmax  11508  2zinfmin  11525  xrmaxifle  11528  xrmaxiflemab  11529  xrmaxiflemlub  11530  xrmaxiflemcom  11531  sumdc  11640  sumrbdclem  11659  fsum3cvg  11660  summodclem2a  11663  zsumdc  11666  isumss  11673  fisumss  11674  isumss2  11675  fsumadd  11688  sumsplitdc  11714  fsummulc2  11730  prodrbdclem  11853  fproddccvg  11854  zproddc  11861  prod1dc  11868  prodssdc  11871  fprodssdc  11872  fprodmul  11873  fprodsplitdc  11878  dvdsabseq  12129  bitsmod  12238  gcdval  12251  gcddvds  12255  gcdcl  12258  gcd0id  12271  gcdneg  12274  gcdaddm  12276  dfgcd3  12302  dfgcd2  12306  gcdmultiplez  12313  dvdssq  12323  dvdslcm  12362  lcmcl  12365  lcmneg  12367  lcmgcd  12371  lcmdvds  12372  lcmid  12373  mulgcddvds  12387  cncongr2  12397  prmind2  12413  rpexp  12446  pw2dvdslemn  12458  fermltl  12527  pclemdc  12582  pcxcl  12605  pcgcd  12623  pcmptcl  12636  pcmpt  12637  pcmpt2  12638  pcprod  12640  fldivp1  12642  1arith  12661  unennn  12739  ennnfonelemss  12752  ennnfonelemkh  12754  ennnfonelemhf1o  12755  ctiunctlemudc  12779  gsumfzz  13298  gsumfzcl  13302  gsumfzreidx  13644  gsumfzsubmcl  13645  gsumfzmptfidmadd  13646  gsumfzmhm  13650  gsumfzfsum  14321  znf1o  14384  lgslem4  15451  lgsneg  15472  lgsmod  15474  lgsdilem  15475  lgsdir2  15481  lgsdir  15483  lgsdi  15485  lgsne0  15486  lgsdirnn0  15495  lgsdinn0  15496  gausslemma2dlem1a  15506  gausslemma2dlem1f1o  15508  lgsquadlem2  15526  lgsquad3  15532  2lgs  15552  sumdc2  15697  2omap  15894  nnsf  15904  nninfsellemsuc  15911  nninffeq  15919  apdifflemr  15948  nconstwlpolem  15966