Theorem exmiddc 838

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 710  DECID wdc 836

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 837

This theorem is referenced by:  stdcndcOLD  848  modc  2097  rabxmdc  3492  dcun  3570  ifsbdc  3583  ifcldadc  3600  ifeq1dadc  3601  ifeq2dadc  3602  ifeqdadc  3603  ifbothdadc  3604  ifbothdc  3605  ifiddc  3606  eqifdc  3607  ifordc  3611  exmid1dc  4244  exmidn0m  4245  exmidundif  4250  exmidundifim  4251  dcextest  4629  dcdifsnid  6590  pw2f1odclem  6931  fidceq  6966  fidifsnen  6967  fimax2gtrilemstep  6997  finexdc  6999  unfiexmid  7015  unsnfidcex  7017  unsnfidcel  7018  undifdcss  7020  prfidceq  7025  tpfidceq  7027  ssfirab  7033  fidcenumlemrks  7055  omp1eomlem  7196  difinfsnlem  7201  difinfsn  7202  ctssdc  7215  nnnninf  7228  nnnninfeq2  7231  nninfisol  7235  exmidomniim  7243  nninfwlpoimlemg  7277  exmidfodomrlemim  7309  netap  7366  2omotaplemap  7369  xaddcom  9983  xnegdi  9990  xpncan  9993  xleadd1a  9995  xsubge0  10003  exfzdc  10369  zsupcllemstep  10372  infssuzex  10376  flqeqceilz  10463  modifeq2int  10531  modfzo0difsn  10540  modsumfzodifsn  10541  iseqf1olemab  10647  iseqf1olemmo  10650  seq3f1olemstep  10659  seqf1oglem1  10664  fser0const  10680  bcval  10894  bccmpl  10899  bcval5  10908  bcpasc  10911  bccl  10912  hashfzp1  10969  ccatsymb  11058  fzowrddc  11100  swrd0g  11113  swrdsbslen  11119  swrdspsleq  11120  2zsupmax  11537  2zinfmin  11554  xrmaxifle  11557  xrmaxiflemab  11558  xrmaxiflemlub  11559  xrmaxiflemcom  11560  sumdc  11669  sumrbdclem  11688  fsum3cvg  11689  summodclem2a  11692  zsumdc  11695  isumss  11702  fisumss  11703  isumss2  11704  fsumadd  11717  sumsplitdc  11743  fsummulc2  11759  prodrbdclem  11882  fproddccvg  11883  zproddc  11890  prod1dc  11897  prodssdc  11900  fprodssdc  11901  fprodmul  11902  fprodsplitdc  11907  dvdsabseq  12158  bitsmod  12267  gcdval  12280  gcddvds  12284  gcdcl  12287  gcd0id  12300  gcdneg  12303  gcdaddm  12305  dfgcd3  12331  dfgcd2  12335  gcdmultiplez  12342  dvdssq  12352  dvdslcm  12391  lcmcl  12394  lcmneg  12396  lcmgcd  12400  lcmdvds  12401  lcmid  12402  mulgcddvds  12416  cncongr2  12426  prmind2  12442  rpexp  12475  pw2dvdslemn  12487  fermltl  12556  pclemdc  12611  pcxcl  12634  pcgcd  12652  pcmptcl  12665  pcmpt  12666  pcmpt2  12667  pcprod  12669  fldivp1  12671  1arith  12690  unennn  12768  ennnfonelemss  12781  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ctiunctlemudc  12808  gsumfzz  13327  gsumfzcl  13331  gsumfzreidx  13673  gsumfzsubmcl  13674  gsumfzmptfidmadd  13675  gsumfzmhm  13679  gsumfzfsum  14350  znf1o  14413  lgslem4  15480  lgsneg  15501  lgsmod  15503  lgsdilem  15504  lgsdir2  15510  lgsdir  15512  lgsdi  15514  lgsne0  15515  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  lgsquadlem2  15555  lgsquad3  15561  2lgs  15581  sumdc2  15735  2omap  15932  nnsf  15942  nninfsellemsuc  15949  nninffeq  15957  apdifflemr  15986  nconstwlpolem  16004