Theorem exmiddc 843

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 715  DECID wdc 841

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 842

This theorem is referenced by:  stdcndcOLD  853  dfifp2dc  989  ifpiddc  999  modc  2123  rabxmdc  3526  dcun  3604  ifsbdc  3618  ifcldadc  3635  ifeq1dadc  3636  ifeq2dadc  3637  ifeqdadc  3638  ifbothdadc  3639  ifbothdc  3640  ifiddc  3641  eqifdc  3642  2if2dc  3645  ifordc  3647  exmid1dc  4290  exmidn0m  4291  exmidundif  4296  exmidundifim  4297  dcextest  4679  dcdifsnid  6672  pw2f1odclem  7020  fidceq  7056  fidifsnen  7057  fidcen  7088  fimax2gtrilemstep  7090  finexdc  7092  elssdc  7094  eqsndc  7095  unfiexmid  7110  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  prfidceq  7120  tpfidceq  7122  ssfirab  7129  fidcenumlemrks  7152  omp1eomlem  7293  difinfsnlem  7298  difinfsn  7299  ctssdc  7312  nnnninf  7325  nnnninfeq2  7328  nninfisol  7332  exmidomniim  7340  nninfwlpoimlemg  7374  exmidfodomrlemim  7412  netap  7473  2omotaplemap  7476  xaddcom  10096  xnegdi  10103  xpncan  10106  xleadd1a  10108  xsubge0  10116  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  flqeqceilz  10581  modifeq2int  10649  modfzo0difsn  10658  modsumfzodifsn  10659  iseqf1olemab  10765  iseqf1olemmo  10768  seq3f1olemstep  10777  seqf1oglem1  10782  fser0const  10798  bcval  11012  bccmpl  11017  bcval5  11026  bcpasc  11029  bccl  11030  hashfzp1  11089  ccatsymb  11183  fzowrddc  11232  swrd0g  11245  swrdsbslen  11251  swrdspsleq  11252  pfxclz  11264  pfxccatin12  11318  swrdccat  11320  pfxccat3a  11323  swrdccat3blem  11324  2zsupmax  11804  2zinfmin  11821  xrmaxifle  11824  xrmaxiflemab  11825  xrmaxiflemlub  11826  xrmaxiflemcom  11827  sumdc  11936  sumrbdclem  11956  fsum3cvg  11957  summodclem2a  11960  zsumdc  11963  isumss  11970  fisumss  11971  isumss2  11972  fsumadd  11985  sumsplitdc  12011  fsummulc2  12027  prodrbdclem  12150  fproddccvg  12151  zproddc  12158  prod1dc  12165  prodssdc  12168  fprodssdc  12169  fprodmul  12170  fprodsplitdc  12175  dvdsabseq  12426  bitsmod  12535  gcdval  12548  gcddvds  12552  gcdcl  12555  gcd0id  12568  gcdneg  12571  gcdaddm  12573  dfgcd3  12599  dfgcd2  12603  gcdmultiplez  12610  dvdssq  12620  dvdslcm  12659  lcmcl  12662  lcmneg  12664  lcmgcd  12668  lcmdvds  12669  lcmid  12670  mulgcddvds  12684  cncongr2  12694  prmind2  12710  rpexp  12743  pw2dvdslemn  12755  fermltl  12824  pclemdc  12879  pcxcl  12902  pcgcd  12920  pcmptcl  12933  pcmpt  12934  pcmpt2  12935  pcprod  12937  fldivp1  12939  1arith  12958  unennn  13036  ennnfonelemss  13049  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ctiunctlemudc  13076  bassetsnn  13157  gsumfzz  13596  gsumfzcl  13600  gsumfzreidx  13942  gsumfzsubmcl  13943  gsumfzmptfidmadd  13944  gsumfzmhm  13948  gsumfzfsum  14621  znf1o  14684  lgslem4  15751  lgsneg  15772  lgsmod  15774  lgsdilem  15775  lgsdir2  15781  lgsdir  15783  lgsdi  15785  lgsne0  15786  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  lgsquadlem2  15826  lgsquad3  15832  2lgs  15852  umgrclwwlkge2  16272  eupth2lem3lem4fi  16343  eupth2lem3lem7fi  16344  sumdc2  16446  2omap  16645  nnsf  16658  nninfsellemsuc  16665  nninffeq  16673  apdifflemr  16702  nconstwlpolem  16721  gsumgfsum  16736