Theorem exmiddc 844

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 716  DECID wdc 842

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 843

This theorem is referenced by:  stdcndcOLD  854  dfifp2dc  990  ifpiddc  1000  modc  2126  rabxmdc  3544  dcun  3623  ifsbdc  3639  ifcldadc  3656  ifeq1dadc  3657  ifeq2dadc  3658  ifeqdadc  3659  ifbothdadc  3660  ifbothdc  3661  ifiddc  3662  eqifdc  3663  2if2dc  3666  ifordc  3668  ifeqeqxdc  3673  exmid1dc  4318  exmidn0m  4319  exmidundif  4324  exmidundifim  4325  dcextest  4708  dcdifsnid  6750  pw2f1odclem  7100  fidceq  7137  fidifsnen  7138  fidcen  7169  fimax2gtrilemstep  7171  finexdc  7173  elssdc  7175  eqsndc  7176  unfiexmid  7191  unsnfidcex  7193  unsnfidcel  7194  undifdcss  7196  prfidceq  7201  tpfidceq  7203  ssfirab  7210  fidcenumlemrks  7236  2omap  7282  omp1eomlem  7398  difinfsnlem  7403  difinfsn  7404  ctssdc  7417  nnnninf  7430  nnnninfeq2  7433  nninfisol  7437  exmidomniim  7445  nninfwlpoimlemg  7479  exmidfodomrlemim  7517  netap  7584  2omotaplemap  7587  xaddcom  10216  xnegdi  10223  xpncan  10226  xleadd1a  10228  xsubge0  10236  exfzdc  10611  zsupcllemstep  10614  infssuzex  10618  flqeqceilz  10707  modifeq2int  10775  modfzo0difsn  10784  modsumfzodifsn  10785  iseqf1olemab  10891  iseqf1olemmo  10894  seq3f1olemstep  10903  seqf1oglem1  10908  fser0const  10924  bcval  11139  bccmpl  11144  bcval5  11153  bcpasc  11156  bccl  11157  hashfzp1  11217  hashfibc  11235  ccatsymb  11318  fzowrddc  11367  swrd0g  11380  swrdsbslen  11386  swrdspsleq  11387  pfxclz  11399  pfxccatin12  11453  swrdccat  11455  pfxccat3a  11458  swrdccat3blem  11459  2zsupmax  11939  2zinfmin  11956  xrmaxifle  11959  xrmaxiflemab  11960  xrmaxiflemlub  11961  xrmaxiflemcom  11962  sumdc  12071  sumrbdclem  12091  fsum3cvg  12092  summodclem2a  12095  zsumdc  12098  isumss  12105  fisumss  12106  isumss2  12107  fsumadd  12120  sumsplitdc  12146  fsummulc2  12162  prodrbdclem  12285  fproddccvg  12286  zproddc  12293  prod1dc  12300  prodssdc  12303  fprodssdc  12304  fprodmul  12305  fprodsplitdc  12310  dvdsabseq  12561  bitsmod  12670  gcdval  12683  gcddvds  12687  gcdcl  12690  gcd0id  12703  gcdneg  12706  gcdaddm  12708  dfgcd3  12734  dfgcd2  12738  gcdmultiplez  12745  dvdssq  12755  dvdslcm  12794  lcmcl  12797  lcmneg  12799  lcmgcd  12803  lcmdvds  12804  lcmid  12805  mulgcddvds  12819  cncongr2  12829  prmind2  12845  rpexp  12878  pw2dvdslemn  12890  fermltl  12959  pclemdc  13014  pcxcl  13037  pcgcd  13055  pcmptcl  13068  pcmpt  13069  pcmpt2  13070  pcprod  13072  fldivp1  13074  1arith  13093  unennn  13235  ennnfonelemss  13248  ennnfonelemkh  13250  ennnfonelemhf1o  13251  ctiunctlemudc  13275  bassetsnn  13356  gsumfzz  13753  gsumfzcl  13757  gsumfzreidx  14093  gsumfzsubmcl  14094  gsumfzmptfidmadd  14095  gsumfzmhm  14099  gsumgfsum  14109  gsumfzfsum  14865  znf1o  14928  lgslem4  16005  lgsneg  16026  lgsmod  16028  lgsdilem  16029  lgsdir2  16035  lgsdir  16037  lgsdi  16039  lgsne0  16040  lgsdirnn0  16049  lgsdinn0  16050  gausslemma2dlem1a  16060  gausslemma2dlem1f1o  16062  lgsquadlem2  16080  lgsquad3  16086  2lgs  16106  umgrclwwlkge2  16526  eupth2lem3lem4fi  16597  eupth2lem3lem7fi  16598  sumdc2  16710  nnsf  16922  nninfsellemsuc  16929  nninffeq  16937  apdifflemr  16970  trimul0or  16984  nconstwlpolem  16990