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  10273  xnegdi  10280  xpncan  10283  xleadd1a  10285  xsubge0  10293  exfzdc  10669  zsupcllemstep  10672  infssuzex  10676  flqeqceilz  10768  modifeq2int  10836  modfzo0difsn  10845  modsumfzodifsn  10846  iseqf1olemab  10952  iseqf1olemmo  10955  seq3f1olemstep  10964  seqf1oglem1  10969  fser0const  10985  bcval  11201  bccmpl  11206  bcval5  11215  bcpasc  11218  bccl  11219  hashfzp1  11279  hashfibc  11297  ccatsymb  11384  fzowrddc  11433  swrd0g  11446  swrdsbslen  11452  swrdspsleq  11453  pfxclz  11465  pfxccatin12  11519  swrdccat  11521  pfxccat3a  11524  swrdccat3blem  11525  2zsupmax  12007  2zinfmin  12025  xrmaxifle  12028  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxiflemcom  12031  sumdc  12140  sumrbdclem  12160  fsum3cvg  12161  summodclem2a  12164  zsumdc  12167  isumss  12174  fisumss  12175  isumss2  12176  fsumadd  12189  sumsplitdc  12215  fsummulc2  12231  prodrbdclem  12354  fproddccvg  12355  zproddc  12362  prod1dc  12369  prodssdc  12372  fprodssdc  12373  fprodmul  12374  fprodsplitdc  12379  dvdsabseq  12630  bitsmod  12739  gcdval  12752  gcddvds  12756  gcdcl  12759  gcd0id  12772  gcdneg  12775  gcdaddm  12777  dfgcd3  12803  dfgcd2  12807  gcdmultiplez  12814  dvdssq  12824  dvdslcm  12863  lcmcl  12866  lcmneg  12868  lcmgcd  12872  lcmdvds  12873  lcmid  12874  mulgcddvds  12888  cncongr2  12898  prmind2  12914  prmdcz  12925  rpexp  12948  pwbdvdslemn  12960  nn0sqdcq  13004  sqrtrirr  13005  fermltl  13032  pclemdc  13087  pcxcl  13110  pcgcd  13128  pcmptcl  13141  pcmpt  13142  pcmpt2  13143  pcprod  13145  fldivp1  13147  1arith  13166  unennn  13337  ennnfonelemss  13350  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ctiunctlemudc  13377  bassetsnn  13458  gzsumcl  13853  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  gzsumgsum  14204  znf1o  15035  ppiqp1le  16173  bposlem1  16209  bposlem3  16211  bposlem5  16213  lgslem4  16220  lgsneg  16241  lgsmod  16243  lgsdilem  16244  lgsdir2  16250  lgsdir  16252  lgsdi  16254  lgsne0  16255  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  lgsquadlem2  16295  lgsquad3  16301  2lgs  16321  umgrclwwlkge2  16741  eupth2lem3lem4fi  16812  eupth2lem3lem7fi  16813  sumdc2  16925  wexmiddifxy  17144  nnsf  17146  nninfsellemsuc  17153  nninffeq  17161  apdifflemr  17194  nconstwlpolem  17213