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  2088  rabxmdc  3483  dcun  3561  ifsbdc  3574  ifcldadc  3591  ifeq1dadc  3592  ifeq2dadc  3593  ifbothdadc  3594  ifbothdc  3595  ifiddc  3596  eqifdc  3597  ifordc  3601  exmid1dc  4234  exmidn0m  4235  exmidundif  4240  exmidundifim  4241  dcextest  4618  dcdifsnid  6571  pw2f1odclem  6904  fidceq  6939  fidifsnen  6940  fimax2gtrilemstep  6970  finexdc  6972  unfiexmid  6988  unsnfidcex  6990  unsnfidcel  6991  undifdcss  6993  prfidceq  6998  tpfidceq  7000  ssfirab  7006  fidcenumlemrks  7028  omp1eomlem  7169  difinfsnlem  7174  difinfsn  7175  ctssdc  7188  nnnninf  7201  nnnninfeq2  7204  nninfisol  7208  exmidomniim  7216  nninfwlpoimlemg  7250  exmidfodomrlemim  7280  netap  7337  2omotaplemap  7340  xaddcom  9953  xnegdi  9960  xpncan  9963  xleadd1a  9965  xsubge0  9973  exfzdc  10333  zsupcllemstep  10336  infssuzex  10340  flqeqceilz  10427  modifeq2int  10495  modfzo0difsn  10504  modsumfzodifsn  10505  iseqf1olemab  10611  iseqf1olemmo  10614  seq3f1olemstep  10623  seqf1oglem1  10628  fser0const  10644  bcval  10858  bccmpl  10863  bcval5  10872  bcpasc  10875  bccl  10876  hashfzp1  10933  2zsupmax  11408  2zinfmin  11425  xrmaxifle  11428  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxiflemcom  11431  sumdc  11540  sumrbdclem  11559  fsum3cvg  11560  summodclem2a  11563  zsumdc  11566  isumss  11573  fisumss  11574  isumss2  11575  fsumadd  11588  sumsplitdc  11614  fsummulc2  11630  prodrbdclem  11753  fproddccvg  11754  zproddc  11761  prod1dc  11768  prodssdc  11771  fprodssdc  11772  fprodmul  11773  fprodsplitdc  11778  dvdsabseq  12029  bitsmod  12138  gcdval  12151  gcddvds  12155  gcdcl  12158  gcd0id  12171  gcdneg  12174  gcdaddm  12176  dfgcd3  12202  dfgcd2  12206  gcdmultiplez  12213  dvdssq  12223  dvdslcm  12262  lcmcl  12265  lcmneg  12267  lcmgcd  12271  lcmdvds  12272  lcmid  12273  mulgcddvds  12287  cncongr2  12297  prmind2  12313  rpexp  12346  pw2dvdslemn  12358  fermltl  12427  pclemdc  12482  pcxcl  12505  pcgcd  12523  pcmptcl  12536  pcmpt  12537  pcmpt2  12538  pcprod  12540  fldivp1  12542  1arith  12561  unennn  12639  ennnfonelemss  12652  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ctiunctlemudc  12679  gsumfzz  13197  gsumfzcl  13201  gsumfzreidx  13543  gsumfzsubmcl  13544  gsumfzmptfidmadd  13545  gsumfzmhm  13549  gsumfzfsum  14220  znf1o  14283  lgslem4  15328  lgsneg  15349  lgsmod  15351  lgsdilem  15352  lgsdir2  15358  lgsdir  15360  lgsdi  15362  lgsne0  15363  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  lgsquadlem2  15403  lgsquad3  15409  2lgs  15429  sumdc2  15529  2omap  15726  nnsf  15736  nninfsellemsuc  15743  nninffeq  15751  apdifflemr  15778  nconstwlpolem  15796