Theorem exmiddc 836

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 708  DECID wdc 834

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 835

This theorem is referenced by:  stdcndcOLD  846  modc  2069  rabxmdc  3454  dcun  3533  ifsbdc  3546  ifcldadc  3563  ifeq1dadc  3564  ifeq2dadc  3565  ifbothdadc  3566  ifbothdc  3567  ifiddc  3568  eqifdc  3569  ifordc  3573  exmid1dc  4200  exmidn0m  4201  exmidundif  4206  exmidundifim  4207  dcextest  4580  dcdifsnid  6504  fidceq  6868  fidifsnen  6869  fimax2gtrilemstep  6899  finexdc  6901  unfiexmid  6916  unsnfidcex  6918  unsnfidcel  6919  undifdcss  6921  ssfirab  6932  fidcenumlemrks  6951  omp1eomlem  7092  difinfsnlem  7097  difinfsn  7098  ctssdc  7111  nnnninf  7123  nnnninfeq2  7126  nninfisol  7130  exmidomniim  7138  nninfwlpoimlemg  7172  exmidfodomrlemim  7199  netap  7252  2omotaplemap  7255  xaddcom  9860  xnegdi  9867  xpncan  9870  xleadd1a  9872  xsubge0  9880  exfzdc  10239  flqeqceilz  10317  modifeq2int  10385  modfzo0difsn  10394  modsumfzodifsn  10395  iseqf1olemab  10488  iseqf1olemmo  10491  seq3f1olemstep  10500  fser0const  10515  bcval  10728  bccmpl  10733  bcval5  10742  bcpasc  10745  bccl  10746  hashfzp1  10803  2zsupmax  11233  2zinfmin  11250  xrmaxifle  11253  xrmaxiflemab  11254  xrmaxiflemlub  11255  xrmaxiflemcom  11256  sumdc  11365  sumrbdclem  11384  fsum3cvg  11385  summodclem2a  11388  zsumdc  11391  isumss  11398  fisumss  11399  isumss2  11400  fsumadd  11413  sumsplitdc  11439  fsummulc2  11455  prodrbdclem  11578  fproddccvg  11579  zproddc  11586  prod1dc  11593  prodssdc  11596  fprodssdc  11597  fprodmul  11598  fprodsplitdc  11603  dvdsabseq  11852  zsupcllemstep  11945  infssuzex  11949  gcdval  11959  gcddvds  11963  gcdcl  11966  gcd0id  11979  gcdneg  11982  gcdaddm  11984  dfgcd3  12010  dfgcd2  12014  gcdmultiplez  12021  dvdssq  12031  dvdslcm  12068  lcmcl  12071  lcmneg  12073  lcmgcd  12077  lcmdvds  12078  lcmid  12079  mulgcddvds  12093  cncongr2  12103  prmind2  12119  rpexp  12152  pw2dvdslemn  12164  fermltl  12233  pclemdc  12287  pcxcl  12310  pcgcd  12327  pcmptcl  12339  pcmpt  12340  pcmpt2  12341  pcprod  12343  fldivp1  12345  1arith  12364  unennn  12397  ennnfonelemss  12410  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ctiunctlemudc  12437  lgslem4  14374  lgsneg  14395  lgsmod  14397  lgsdilem  14398  lgsdir2  14404  lgsdir  14406  lgsdi  14408  lgsne0  14409  lgsdirnn0  14418  lgsdinn0  14419  sumdc2  14521  nnsf  14724  nninfsellemsuc  14731  nninffeq  14739  apdifflemr  14765  nconstwlpolem  14782