Theorem exmiddc 841

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 713  DECID wdc 839

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 840

This theorem is referenced by:  stdcndcOLD  851  dfifp2dc  987  ifpiddc  997  modc  2121  rabxmdc  3524  dcun  3602  ifsbdc  3616  ifcldadc  3633  ifeq1dadc  3634  ifeq2dadc  3635  ifeqdadc  3636  ifbothdadc  3637  ifbothdc  3638  ifiddc  3639  eqifdc  3640  2if2dc  3643  ifordc  3645  exmid1dc  4288  exmidn0m  4289  exmidundif  4294  exmidundifim  4295  dcextest  4677  dcdifsnid  6667  pw2f1odclem  7015  fidceq  7051  fidifsnen  7052  fidcen  7081  fimax2gtrilemstep  7083  finexdc  7085  elssdc  7087  eqsndc  7088  unfiexmid  7103  unsnfidcex  7105  unsnfidcel  7106  undifdcss  7108  prfidceq  7113  tpfidceq  7115  ssfirab  7121  fidcenumlemrks  7143  omp1eomlem  7284  difinfsnlem  7289  difinfsn  7290  ctssdc  7303  nnnninf  7316  nnnninfeq2  7319  nninfisol  7323  exmidomniim  7331  nninfwlpoimlemg  7365  exmidfodomrlemim  7402  netap  7463  2omotaplemap  7466  xaddcom  10086  xnegdi  10093  xpncan  10096  xleadd1a  10098  xsubge0  10106  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  flqeqceilz  10570  modifeq2int  10638  modfzo0difsn  10647  modsumfzodifsn  10648  iseqf1olemab  10754  iseqf1olemmo  10757  seq3f1olemstep  10766  seqf1oglem1  10771  fser0const  10787  bcval  11001  bccmpl  11006  bcval5  11015  bcpasc  11018  bccl  11019  hashfzp1  11078  ccatsymb  11169  fzowrddc  11218  swrd0g  11231  swrdsbslen  11237  swrdspsleq  11238  pfxclz  11250  pfxccatin12  11304  swrdccat  11306  pfxccat3a  11309  swrdccat3blem  11310  2zsupmax  11777  2zinfmin  11794  xrmaxifle  11797  xrmaxiflemab  11798  xrmaxiflemlub  11799  xrmaxiflemcom  11800  sumdc  11909  sumrbdclem  11928  fsum3cvg  11929  summodclem2a  11932  zsumdc  11935  isumss  11942  fisumss  11943  isumss2  11944  fsumadd  11957  sumsplitdc  11983  fsummulc2  11999  prodrbdclem  12122  fproddccvg  12123  zproddc  12130  prod1dc  12137  prodssdc  12140  fprodssdc  12141  fprodmul  12142  fprodsplitdc  12147  dvdsabseq  12398  bitsmod  12507  gcdval  12520  gcddvds  12524  gcdcl  12527  gcd0id  12540  gcdneg  12543  gcdaddm  12545  dfgcd3  12571  dfgcd2  12575  gcdmultiplez  12582  dvdssq  12592  dvdslcm  12631  lcmcl  12634  lcmneg  12636  lcmgcd  12640  lcmdvds  12641  lcmid  12642  mulgcddvds  12656  cncongr2  12666  prmind2  12682  rpexp  12715  pw2dvdslemn  12727  fermltl  12796  pclemdc  12851  pcxcl  12874  pcgcd  12892  pcmptcl  12905  pcmpt  12906  pcmpt2  12907  pcprod  12909  fldivp1  12911  1arith  12930  unennn  13008  ennnfonelemss  13021  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ctiunctlemudc  13048  bassetsnn  13129  gsumfzz  13568  gsumfzcl  13572  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  gsumfzfsum  14592  znf1o  14655  lgslem4  15722  lgsneg  15743  lgsmod  15745  lgsdilem  15746  lgsdir2  15752  lgsdir  15754  lgsdi  15756  lgsne0  15757  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  lgsquadlem2  15797  lgsquad3  15803  2lgs  15823  umgrclwwlkge2  16197  sumdc2  16331  2omap  16530  nnsf  16543  nninfsellemsuc  16550  nninffeq  16558  apdifflemr  16587  nconstwlpolem  16605