Theorem exmiddc 837

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 836	. 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2	1	biimpi 120	1 ⊢ (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 709  DECID wdc 835

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 836

This theorem is referenced by:  stdcndcOLD  847  modc  2079  rabxmdc  3466  dcun  3545  ifsbdc  3558  ifcldadc  3575  ifeq1dadc  3576  ifeq2dadc  3577  ifbothdadc  3578  ifbothdc  3579  ifiddc  3580  eqifdc  3581  ifordc  3585  exmid1dc  4212  exmidn0m  4213  exmidundif  4218  exmidundifim  4219  dcextest  4592  dcdifsnid  6519  fidceq  6883  fidifsnen  6884  fimax2gtrilemstep  6914  finexdc  6916  unfiexmid  6931  unsnfidcex  6933  unsnfidcel  6934  undifdcss  6936  ssfirab  6947  fidcenumlemrks  6966  omp1eomlem  7107  difinfsnlem  7112  difinfsn  7113  ctssdc  7126  nnnninf  7138  nnnninfeq2  7141  nninfisol  7145  exmidomniim  7153  nninfwlpoimlemg  7187  exmidfodomrlemim  7214  netap  7267  2omotaplemap  7270  xaddcom  9875  xnegdi  9882  xpncan  9885  xleadd1a  9887  xsubge0  9895  exfzdc  10254  flqeqceilz  10332  modifeq2int  10400  modfzo0difsn  10409  modsumfzodifsn  10410  iseqf1olemab  10503  iseqf1olemmo  10506  seq3f1olemstep  10515  fser0const  10530  bcval  10743  bccmpl  10748  bcval5  10757  bcpasc  10760  bccl  10761  hashfzp1  10818  2zsupmax  11248  2zinfmin  11265  xrmaxifle  11268  xrmaxiflemab  11269  xrmaxiflemlub  11270  xrmaxiflemcom  11271  sumdc  11380  sumrbdclem  11399  fsum3cvg  11400  summodclem2a  11403  zsumdc  11406  isumss  11413  fisumss  11414  isumss2  11415  fsumadd  11428  sumsplitdc  11454  fsummulc2  11470  prodrbdclem  11593  fproddccvg  11594  zproddc  11601  prod1dc  11608  prodssdc  11611  fprodssdc  11612  fprodmul  11613  fprodsplitdc  11618  dvdsabseq  11867  zsupcllemstep  11960  infssuzex  11964  gcdval  11974  gcddvds  11978  gcdcl  11981  gcd0id  11994  gcdneg  11997  gcdaddm  11999  dfgcd3  12025  dfgcd2  12029  gcdmultiplez  12036  dvdssq  12046  dvdslcm  12083  lcmcl  12086  lcmneg  12088  lcmgcd  12092  lcmdvds  12093  lcmid  12094  mulgcddvds  12108  cncongr2  12118  prmind2  12134  rpexp  12167  pw2dvdslemn  12179  fermltl  12248  pclemdc  12302  pcxcl  12325  pcgcd  12342  pcmptcl  12354  pcmpt  12355  pcmpt2  12356  pcprod  12358  fldivp1  12360  1arith  12379  unennn  12412  ennnfonelemss  12425  ennnfonelemkh  12427  ennnfonelemhf1o  12428  ctiunctlemudc  12452  lgslem4  14700  lgsneg  14721  lgsmod  14723  lgsdilem  14724  lgsdir2  14730  lgsdir  14732  lgsdi  14734  lgsne0  14735  lgsdirnn0  14744  lgsdinn0  14745  sumdc2  14847  nnsf  15051  nninfsellemsuc  15058  nninffeq  15066  apdifflemr  15092  nconstwlpolem  15110