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  3523  dcun  3601  ifsbdc  3615  ifcldadc  3632  ifeq1dadc  3633  ifeq2dadc  3634  ifeqdadc  3635  ifbothdadc  3636  ifbothdc  3637  ifiddc  3638  eqifdc  3639  2if2dc  3642  ifordc  3644  exmid1dc  4284  exmidn0m  4285  exmidundif  4290  exmidundifim  4291  dcextest  4673  dcdifsnid  6658  pw2f1odclem  7003  fidceq  7039  fidifsnen  7040  fidcen  7069  fimax2gtrilemstep  7071  finexdc  7073  elssdc  7075  eqsndc  7076  unfiexmid  7091  unsnfidcex  7093  unsnfidcel  7094  undifdcss  7096  prfidceq  7101  tpfidceq  7103  ssfirab  7109  fidcenumlemrks  7131  omp1eomlem  7272  difinfsnlem  7277  difinfsn  7278  ctssdc  7291  nnnninf  7304  nnnninfeq2  7307  nninfisol  7311  exmidomniim  7319  nninfwlpoimlemg  7353  exmidfodomrlemim  7390  netap  7451  2omotaplemap  7454  xaddcom  10069  xnegdi  10076  xpncan  10079  xleadd1a  10081  xsubge0  10089  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  flqeqceilz  10552  modifeq2int  10620  modfzo0difsn  10629  modsumfzodifsn  10630  iseqf1olemab  10736  iseqf1olemmo  10739  seq3f1olemstep  10748  seqf1oglem1  10753  fser0const  10769  bcval  10983  bccmpl  10988  bcval5  10997  bcpasc  11000  bccl  11001  hashfzp1  11059  ccatsymb  11150  fzowrddc  11194  swrd0g  11207  swrdsbslen  11213  swrdspsleq  11214  pfxclz  11226  pfxccatin12  11280  swrdccat  11282  pfxccat3a  11285  swrdccat3blem  11286  2zsupmax  11752  2zinfmin  11769  xrmaxifle  11772  xrmaxiflemab  11773  xrmaxiflemlub  11774  xrmaxiflemcom  11775  sumdc  11884  sumrbdclem  11903  fsum3cvg  11904  summodclem2a  11907  zsumdc  11910  isumss  11917  fisumss  11918  isumss2  11919  fsumadd  11932  sumsplitdc  11958  fsummulc2  11974  prodrbdclem  12097  fproddccvg  12098  zproddc  12105  prod1dc  12112  prodssdc  12115  fprodssdc  12116  fprodmul  12117  fprodsplitdc  12122  dvdsabseq  12373  bitsmod  12482  gcdval  12495  gcddvds  12499  gcdcl  12502  gcd0id  12515  gcdneg  12518  gcdaddm  12520  dfgcd3  12546  dfgcd2  12550  gcdmultiplez  12557  dvdssq  12567  dvdslcm  12606  lcmcl  12609  lcmneg  12611  lcmgcd  12615  lcmdvds  12616  lcmid  12617  mulgcddvds  12631  cncongr2  12641  prmind2  12657  rpexp  12690  pw2dvdslemn  12702  fermltl  12771  pclemdc  12826  pcxcl  12849  pcgcd  12867  pcmptcl  12880  pcmpt  12881  pcmpt2  12882  pcprod  12884  fldivp1  12886  1arith  12905  unennn  12983  ennnfonelemss  12996  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ctiunctlemudc  13023  bassetsnn  13104  gsumfzz  13543  gsumfzcl  13547  gsumfzreidx  13889  gsumfzsubmcl  13890  gsumfzmptfidmadd  13891  gsumfzmhm  13895  gsumfzfsum  14567  znf1o  14630  lgslem4  15697  lgsneg  15718  lgsmod  15720  lgsdilem  15721  lgsdir2  15727  lgsdir  15729  lgsdi  15731  lgsne0  15732  lgsdirnn0  15741  lgsdinn0  15742  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  lgsquadlem2  15772  lgsquad3  15778  2lgs  15798  umgrclwwlkge2  16139  sumdc2  16218  2omap  16418  nnsf  16431  nninfsellemsuc  16438  nninffeq  16446  apdifflemr  16475  nconstwlpolem  16493