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  2085  rabxmdc  3478  dcun  3556  ifsbdc  3569  ifcldadc  3586  ifeq1dadc  3587  ifeq2dadc  3588  ifbothdadc  3589  ifbothdc  3590  ifiddc  3591  eqifdc  3592  ifordc  3596  exmid1dc  4229  exmidn0m  4230  exmidundif  4235  exmidundifim  4236  dcextest  4613  dcdifsnid  6557  pw2f1odclem  6890  fidceq  6925  fidifsnen  6926  fimax2gtrilemstep  6956  finexdc  6958  unfiexmid  6974  unsnfidcex  6976  unsnfidcel  6977  undifdcss  6979  ssfirab  6990  fidcenumlemrks  7012  omp1eomlem  7153  difinfsnlem  7158  difinfsn  7159  ctssdc  7172  nnnninf  7185  nnnninfeq2  7188  nninfisol  7192  exmidomniim  7200  nninfwlpoimlemg  7234  exmidfodomrlemim  7261  netap  7314  2omotaplemap  7317  xaddcom  9927  xnegdi  9934  xpncan  9937  xleadd1a  9939  xsubge0  9947  exfzdc  10307  flqeqceilz  10389  modifeq2int  10457  modfzo0difsn  10466  modsumfzodifsn  10467  iseqf1olemab  10573  iseqf1olemmo  10576  seq3f1olemstep  10585  seqf1oglem1  10590  fser0const  10606  bcval  10820  bccmpl  10825  bcval5  10834  bcpasc  10837  bccl  10838  hashfzp1  10895  2zsupmax  11369  2zinfmin  11386  xrmaxifle  11389  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxiflemcom  11392  sumdc  11501  sumrbdclem  11520  fsum3cvg  11521  summodclem2a  11524  zsumdc  11527  isumss  11534  fisumss  11535  isumss2  11536  fsumadd  11549  sumsplitdc  11575  fsummulc2  11591  prodrbdclem  11714  fproddccvg  11715  zproddc  11722  prod1dc  11729  prodssdc  11732  fprodssdc  11733  fprodmul  11734  fprodsplitdc  11739  dvdsabseq  11989  zsupcllemstep  12082  infssuzex  12086  gcdval  12096  gcddvds  12100  gcdcl  12103  gcd0id  12116  gcdneg  12119  gcdaddm  12121  dfgcd3  12147  dfgcd2  12151  gcdmultiplez  12158  dvdssq  12168  dvdslcm  12207  lcmcl  12210  lcmneg  12212  lcmgcd  12216  lcmdvds  12217  lcmid  12218  mulgcddvds  12232  cncongr2  12242  prmind2  12258  rpexp  12291  pw2dvdslemn  12303  fermltl  12372  pclemdc  12426  pcxcl  12449  pcgcd  12467  pcmptcl  12480  pcmpt  12481  pcmpt2  12482  pcprod  12484  fldivp1  12486  1arith  12505  unennn  12554  ennnfonelemss  12567  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ctiunctlemudc  12594  gsumfzz  13067  gsumfzcl  13071  gsumfzreidx  13407  gsumfzsubmcl  13408  gsumfzmptfidmadd  13409  gsumfzmhm  13413  gsumfzfsum  14076  znf1o  14139  lgslem4  15119  lgsneg  15140  lgsmod  15142  lgsdilem  15143  lgsdir2  15149  lgsdir  15151  lgsdi  15153  lgsne0  15154  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  sumdc2  15291  nnsf  15495  nninfsellemsuc  15502  nninffeq  15510  apdifflemr  15537  nconstwlpolem  15555