Theorem exmiddc 836

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 708  DECID wdc 834

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 835

This theorem is referenced by:  stdcndcOLD  846  modc  2069  rabxmdc  3454  dcun  3533  ifsbdc  3546  ifcldadc  3563  ifeq1dadc  3564  ifeq2dadc  3565  ifbothdadc  3566  ifbothdc  3567  ifiddc  3568  eqifdc  3569  ifordc  3573  exmid1dc  4198  exmidn0m  4199  exmidundif  4204  exmidundifim  4205  dcextest  4578  dcdifsnid  6500  fidceq  6864  fidifsnen  6865  fimax2gtrilemstep  6895  finexdc  6897  unfiexmid  6912  unsnfidcex  6914  unsnfidcel  6915  undifdcss  6917  ssfirab  6928  fidcenumlemrks  6947  omp1eomlem  7088  difinfsnlem  7093  difinfsn  7094  ctssdc  7107  nnnninf  7119  nnnninfeq2  7122  nninfisol  7126  exmidomniim  7134  nninfwlpoimlemg  7168  exmidfodomrlemim  7195  netap  7248  2omotaplemap  7251  xaddcom  9855  xnegdi  9862  xpncan  9865  xleadd1a  9867  xsubge0  9875  exfzdc  10233  flqeqceilz  10311  modifeq2int  10379  modfzo0difsn  10388  modsumfzodifsn  10389  iseqf1olemab  10482  iseqf1olemmo  10485  seq3f1olemstep  10494  fser0const  10509  bcval  10720  bccmpl  10725  bcval5  10734  bcpasc  10737  bccl  10738  hashfzp1  10795  2zsupmax  11225  2zinfmin  11242  xrmaxifle  11245  xrmaxiflemab  11246  xrmaxiflemlub  11247  xrmaxiflemcom  11248  sumdc  11357  sumrbdclem  11376  fsum3cvg  11377  summodclem2a  11380  zsumdc  11383  isumss  11390  fisumss  11391  isumss2  11392  fsumadd  11405  sumsplitdc  11431  fsummulc2  11447  prodrbdclem  11570  fproddccvg  11571  zproddc  11578  prod1dc  11585  prodssdc  11588  fprodssdc  11589  fprodmul  11590  fprodsplitdc  11595  dvdsabseq  11843  zsupcllemstep  11936  infssuzex  11940  gcdval  11950  gcddvds  11954  gcdcl  11957  gcd0id  11970  gcdneg  11973  gcdaddm  11975  dfgcd3  12001  dfgcd2  12005  gcdmultiplez  12012  dvdssq  12022  dvdslcm  12059  lcmcl  12062  lcmneg  12064  lcmgcd  12068  lcmdvds  12069  lcmid  12070  mulgcddvds  12084  cncongr2  12094  prmind2  12110  rpexp  12143  pw2dvdslemn  12155  fermltl  12224  pclemdc  12278  pcxcl  12301  pcgcd  12318  pcmptcl  12330  pcmpt  12331  pcmpt2  12332  pcprod  12334  fldivp1  12336  1arith  12355  unennn  12388  ennnfonelemss  12401  ennnfonelemkh  12403  ennnfonelemhf1o  12404  ctiunctlemudc  12428  lgslem4  14186  lgsneg  14207  lgsmod  14209  lgsdilem  14210  lgsdir2  14216  lgsdir  14218  lgsdi  14220  lgsne0  14221  lgsdirnn0  14230  lgsdinn0  14231  sumdc2  14322  nnsf  14525  nninfsellemsuc  14532  nninffeq  14540  apdifflemr  14566  nconstwlpolem  14583