Theorem exmiddc 848

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

This proof depends on syntax axioms:   -. wn 3   -> wi 4   \/ wo 720  DECID wdc 846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-dc 847

This theorem is used by:  stdcndcOLD  858  dfifp2dc  994  ifpiddc  1004  modc  2130  rabxmdc  3554  dcun  3637  ifsbdc  3653  ifcldadc  3670  ifeq1dadc  3671  ifeq2dadc  3672  ifeqdadc  3673  ifbothdadc  3674  ifbothdc  3675  ifiddc  3676  eqifdc  3677  2if2dc  3680  ifordc  3682  ifeqeqxdc  3687  exmid1dc  4337  exmidn0m  4338  exmidundif  4343  exmidundifim  4344  dcextest  4728  dcdifsnid  6777  pw2f1odclem  7134  fidceq  7171  fidifsnen  7172  fidcen  7203  fimax2gtrilemstep  7205  finexdc  7207  elssdc  7209  eqsndc  7210  unfiexmid  7225  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  prfidceq  7235  tpfidceq  7237  ssfirab  7244  fidcenumlemrks  7270  2omap  7318  omp1eomlem  7434  difinfsnlem  7439  difinfsn  7440  ctssdc  7453  nnnninf  7466  nnnninfeq2  7469  nninfisol  7473  exmidomniim  7481  nninfwlpoimlemg  7515  exmidfodomrlemim  7553  netap  7620  2omotaplemap  7623  xaddcom  10263  xnegdi  10270  xpncan  10273  xleadd1a  10275  xsubge0  10283  exfzdc  10659  zsupcllemstep  10662  infssuzex  10666  flqeqceilz  10755  modifeq2int  10823  modfzo0difsn  10832  modsumfzodifsn  10833  iseqf1olemab  10939  iseqf1olemmo  10942  seq3f1olemstep  10951  seqf1oglem1  10956  fser0const  10972  bcval  11187  bccmpl  11192  bcval5  11201  bcpasc  11204  bccl  11205  hashfzp1  11265  hashfibc  11283  ccatsymb  11370  fzowrddc  11419  swrd0g  11432  swrdsbslen  11438  swrdspsleq  11439  pfxclz  11451  pfxccatin12  11505  swrdccat  11507  pfxccat3a  11510  swrdccat3blem  11511  2zsupmax  11992  2zinfmin  12009  xrmaxifle  12012  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxiflemcom  12015  sumdc  12124  sumrbdclem  12144  fsum3cvg  12145  summodclem2a  12148  zsumdc  12151  isumss  12158  fisumss  12159  isumss2  12160  fsumadd  12173  sumsplitdc  12199  fsummulc2  12215  prodrbdclem  12338  fproddccvg  12339  zproddc  12346  prod1dc  12353  prodssdc  12356  fprodssdc  12357  fprodmul  12358  fprodsplitdc  12363  dvdsabseq  12614  bitsmod  12723  gcdval  12736  gcddvds  12740  gcdcl  12743  gcd0id  12756  gcdneg  12759  gcdaddm  12761  dfgcd3  12787  dfgcd2  12791  gcdmultiplez  12798  dvdssq  12808  dvdslcm  12847  lcmcl  12850  lcmneg  12852  lcmgcd  12856  lcmdvds  12857  lcmid  12858  mulgcddvds  12872  cncongr2  12882  prmind2  12898  rpexp  12931  pw2dvdslemn  12943  fermltl  13012  pclemdc  13067  pcxcl  13090  pcgcd  13108  pcmptcl  13121  pcmpt  13122  pcmpt2  13123  pcprod  13125  fldivp1  13127  1arith  13146  unennn  13288  ennnfonelemss  13301  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ctiunctlemudc  13328  bassetsnn  13409  gzsumcl  13804  gzsumreidx  14141  gzsumsubmcl  14142  gzsummhm  14145  gzsumgsum  14155  znf1o  14986  lgslem4  16122  lgsneg  16143  lgsmod  16145  lgsdilem  16146  lgsdir2  16152  lgsdir  16154  lgsdi  16156  lgsne0  16157  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  lgsquadlem2  16197  lgsquad3  16203  2lgs  16223  umgrclwwlkge2  16643  eupth2lem3lem4fi  16714  eupth2lem3lem7fi  16715  sumdc2  16827  wexmiddifxy  17046  nnsf  17048  nninfsellemsuc  17055  nninffeq  17063  apdifflemr  17096  nconstwlpolem  17115