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 𝜑 → (𝜑 ∨ ¬ 𝜑))

Proof of Theorem exmiddc

Step	Hyp	Ref	Expression
1		df-dc 842	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2	1	biimpi 120	1 ⊢ (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑))

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  2122  rabxmdc  3525  dcun  3603  ifsbdc  3619  ifcldadc  3636  ifeq1dadc  3637  ifeq2dadc  3638  ifeqdadc  3639  ifbothdadc  3640  ifbothdc  3641  ifiddc  3642  eqifdc  3643  2if2dc  3646  ifordc  3648  exmid1dc  4292  exmidn0m  4293  exmidundif  4298  exmidundifim  4299  dcextest  4681  dcdifsnid  6677  pw2f1odclem  7025  fidceq  7061  fidifsnen  7062  fidcen  7093  fimax2gtrilemstep  7095  finexdc  7097  elssdc  7099  eqsndc  7100  unfiexmid  7115  unsnfidcex  7117  unsnfidcel  7118  undifdcss  7120  prfidceq  7125  tpfidceq  7127  ssfirab  7134  fidcenumlemrks  7157  omp1eomlem  7298  difinfsnlem  7303  difinfsn  7304  ctssdc  7317  nnnninf  7330  nnnninfeq2  7333  nninfisol  7337  exmidomniim  7345  nninfwlpoimlemg  7379  exmidfodomrlemim  7417  netap  7478  2omotaplemap  7481  xaddcom  10101  xnegdi  10108  xpncan  10111  xleadd1a  10113  xsubge0  10121  exfzdc  10492  zsupcllemstep  10495  infssuzex  10499  flqeqceilz  10586  modifeq2int  10654  modfzo0difsn  10663  modsumfzodifsn  10664  iseqf1olemab  10770  iseqf1olemmo  10773  seq3f1olemstep  10782  seqf1oglem1  10787  fser0const  10803  bcval  11017  bccmpl  11022  bcval5  11031  bcpasc  11034  bccl  11035  hashfzp1  11094  ccatsymb  11188  fzowrddc  11237  swrd0g  11250  swrdsbslen  11256  swrdspsleq  11257  pfxclz  11269  pfxccatin12  11323  swrdccat  11325  pfxccat3a  11328  swrdccat3blem  11329  2zsupmax  11809  2zinfmin  11826  xrmaxifle  11829  xrmaxiflemab  11830  xrmaxiflemlub  11831  xrmaxiflemcom  11832  sumdc  11941  sumrbdclem  11961  fsum3cvg  11962  summodclem2a  11965  zsumdc  11968  isumss  11975  fisumss  11976  isumss2  11977  fsumadd  11990  sumsplitdc  12016  fsummulc2  12032  prodrbdclem  12155  fproddccvg  12156  zproddc  12163  prod1dc  12170  prodssdc  12173  fprodssdc  12174  fprodmul  12175  fprodsplitdc  12180  dvdsabseq  12431  bitsmod  12540  gcdval  12553  gcddvds  12557  gcdcl  12560  gcd0id  12573  gcdneg  12576  gcdaddm  12578  dfgcd3  12604  dfgcd2  12608  gcdmultiplez  12615  dvdssq  12625  dvdslcm  12664  lcmcl  12667  lcmneg  12669  lcmgcd  12673  lcmdvds  12674  lcmid  12675  mulgcddvds  12689  cncongr2  12699  prmind2  12715  rpexp  12748  pw2dvdslemn  12760  fermltl  12829  pclemdc  12884  pcxcl  12907  pcgcd  12925  pcmptcl  12938  pcmpt  12939  pcmpt2  12940  pcprod  12942  fldivp1  12944  1arith  12963  unennn  13041  ennnfonelemss  13054  ennnfonelemkh  13056  ennnfonelemhf1o  13057  ctiunctlemudc  13081  bassetsnn  13162  gsumfzz  13601  gsumfzcl  13605  gsumfzreidx  13947  gsumfzsubmcl  13948  gsumfzmptfidmadd  13949  gsumfzmhm  13953  gsumfzfsum  14626  znf1o  14689  lgslem4  15761  lgsneg  15782  lgsmod  15784  lgsdilem  15785  lgsdir2  15791  lgsdir  15793  lgsdi  15795  lgsne0  15796  lgsdirnn0  15805  lgsdinn0  15806  gausslemma2dlem1a  15816  gausslemma2dlem1f1o  15818  lgsquadlem2  15836  lgsquad3  15842  2lgs  15862  umgrclwwlkge2  16282  eupth2lem3lem4fi  16353  eupth2lem3lem7fi  16354  sumdc2  16456  2omap  16654  nnsf  16670  nninfsellemsuc  16677  nninffeq  16685  apdifflemr  16718  nconstwlpolem  16737  gsumgfsum  16752