Theorem exmiddc 838

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 710  DECID wdc 836

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 837

This theorem is referenced by:  stdcndcOLD  848  modc  2098  rabxmdc  3493  dcun  3571  ifsbdc  3584  ifcldadc  3601  ifeq1dadc  3602  ifeq2dadc  3603  ifeqdadc  3604  ifbothdadc  3605  ifbothdc  3606  ifiddc  3607  eqifdc  3608  ifordc  3612  exmid1dc  4248  exmidn0m  4249  exmidundif  4254  exmidundifim  4255  dcextest  4633  dcdifsnid  6597  pw2f1odclem  6938  fidceq  6973  fidifsnen  6974  fimax2gtrilemstep  7004  finexdc  7006  unfiexmid  7022  unsnfidcex  7024  unsnfidcel  7025  undifdcss  7027  prfidceq  7032  tpfidceq  7034  ssfirab  7040  fidcenumlemrks  7062  omp1eomlem  7203  difinfsnlem  7208  difinfsn  7209  ctssdc  7222  nnnninf  7235  nnnninfeq2  7238  nninfisol  7242  exmidomniim  7250  nninfwlpoimlemg  7284  exmidfodomrlemim  7316  netap  7373  2omotaplemap  7376  xaddcom  9990  xnegdi  9997  xpncan  10000  xleadd1a  10002  xsubge0  10010  exfzdc  10376  zsupcllemstep  10379  infssuzex  10383  flqeqceilz  10470  modifeq2int  10538  modfzo0difsn  10547  modsumfzodifsn  10548  iseqf1olemab  10654  iseqf1olemmo  10657  seq3f1olemstep  10666  seqf1oglem1  10671  fser0const  10687  bcval  10901  bccmpl  10906  bcval5  10915  bcpasc  10918  bccl  10919  hashfzp1  10976  ccatsymb  11066  fzowrddc  11108  swrd0g  11121  swrdsbslen  11127  swrdspsleq  11128  2zsupmax  11581  2zinfmin  11598  xrmaxifle  11601  xrmaxiflemab  11602  xrmaxiflemlub  11603  xrmaxiflemcom  11604  sumdc  11713  sumrbdclem  11732  fsum3cvg  11733  summodclem2a  11736  zsumdc  11739  isumss  11746  fisumss  11747  isumss2  11748  fsumadd  11761  sumsplitdc  11787  fsummulc2  11803  prodrbdclem  11926  fproddccvg  11927  zproddc  11934  prod1dc  11941  prodssdc  11944  fprodssdc  11945  fprodmul  11946  fprodsplitdc  11951  dvdsabseq  12202  bitsmod  12311  gcdval  12324  gcddvds  12328  gcdcl  12331  gcd0id  12344  gcdneg  12347  gcdaddm  12349  dfgcd3  12375  dfgcd2  12379  gcdmultiplez  12386  dvdssq  12396  dvdslcm  12435  lcmcl  12438  lcmneg  12440  lcmgcd  12444  lcmdvds  12445  lcmid  12446  mulgcddvds  12460  cncongr2  12470  prmind2  12486  rpexp  12519  pw2dvdslemn  12531  fermltl  12600  pclemdc  12655  pcxcl  12678  pcgcd  12696  pcmptcl  12709  pcmpt  12710  pcmpt2  12711  pcprod  12713  fldivp1  12715  1arith  12734  unennn  12812  ennnfonelemss  12825  ennnfonelemkh  12827  ennnfonelemhf1o  12828  ctiunctlemudc  12852  gsumfzz  13371  gsumfzcl  13375  gsumfzreidx  13717  gsumfzsubmcl  13718  gsumfzmptfidmadd  13719  gsumfzmhm  13723  gsumfzfsum  14394  znf1o  14457  lgslem4  15524  lgsneg  15545  lgsmod  15547  lgsdilem  15548  lgsdir2  15554  lgsdir  15556  lgsdi  15558  lgsne0  15559  lgsdirnn0  15568  lgsdinn0  15569  gausslemma2dlem1a  15579  gausslemma2dlem1f1o  15581  lgsquadlem2  15599  lgsquad3  15605  2lgs  15625  sumdc2  15809  2omap  16006  nnsf  16016  nninfsellemsuc  16023  nninffeq  16031  apdifflemr  16060  nconstwlpolem  16078