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  2124  rabxmdc  3539  dcun  3618  ifsbdc  3634  ifcldadc  3651  ifeq1dadc  3652  ifeq2dadc  3653  ifeqdadc  3654  ifbothdadc  3655  ifbothdc  3656  ifiddc  3657  eqifdc  3658  2if2dc  3661  ifordc  3663  exmid1dc  4312  exmidn0m  4313  exmidundif  4318  exmidundifim  4319  dcextest  4702  dcdifsnid  6736  pw2f1odclem  7086  fidceq  7123  fidifsnen  7124  fidcen  7155  fimax2gtrilemstep  7157  finexdc  7159  elssdc  7161  eqsndc  7162  unfiexmid  7177  unsnfidcex  7179  unsnfidcel  7180  undifdcss  7182  prfidceq  7187  tpfidceq  7189  ssfirab  7196  fidcenumlemrks  7222  2omap  7268  omp1eomlem  7384  difinfsnlem  7389  difinfsn  7390  ctssdc  7403  nnnninf  7416  nnnninfeq2  7419  nninfisol  7423  exmidomniim  7431  nninfwlpoimlemg  7465  exmidfodomrlemim  7503  netap  7564  2omotaplemap  7567  xaddcom  10190  xnegdi  10197  xpncan  10200  xleadd1a  10202  xsubge0  10210  exfzdc  10582  zsupcllemstep  10585  infssuzex  10589  flqeqceilz  10676  modifeq2int  10744  modfzo0difsn  10753  modsumfzodifsn  10754  iseqf1olemab  10860  iseqf1olemmo  10863  seq3f1olemstep  10872  seqf1oglem1  10877  fser0const  10893  bcval  11107  bccmpl  11112  bcval5  11121  bcpasc  11124  bccl  11125  hashfzp1  11184  hashfibc  11200  ccatsymb  11283  fzowrddc  11332  swrd0g  11345  swrdsbslen  11351  swrdspsleq  11352  pfxclz  11364  pfxccatin12  11418  swrdccat  11420  pfxccat3a  11423  swrdccat3blem  11424  2zsupmax  11904  2zinfmin  11921  xrmaxifle  11924  xrmaxiflemab  11925  xrmaxiflemlub  11926  xrmaxiflemcom  11927  sumdc  12036  sumrbdclem  12056  fsum3cvg  12057  summodclem2a  12060  zsumdc  12063  isumss  12070  fisumss  12071  isumss2  12072  fsumadd  12085  sumsplitdc  12111  fsummulc2  12127  prodrbdclem  12250  fproddccvg  12251  zproddc  12258  prod1dc  12265  prodssdc  12268  fprodssdc  12269  fprodmul  12270  fprodsplitdc  12275  dvdsabseq  12526  bitsmod  12635  gcdval  12648  gcddvds  12652  gcdcl  12655  gcd0id  12668  gcdneg  12671  gcdaddm  12673  dfgcd3  12699  dfgcd2  12703  gcdmultiplez  12710  dvdssq  12720  dvdslcm  12759  lcmcl  12762  lcmneg  12764  lcmgcd  12768  lcmdvds  12769  lcmid  12770  mulgcddvds  12784  cncongr2  12794  prmind2  12810  rpexp  12843  pw2dvdslemn  12855  fermltl  12924  pclemdc  12979  pcxcl  13002  pcgcd  13020  pcmptcl  13033  pcmpt  13034  pcmpt2  13035  pcprod  13037  fldivp1  13039  1arith  13058  unennn  13137  ennnfonelemss  13150  ennnfonelemkh  13152  ennnfonelemhf1o  13153  ctiunctlemudc  13177  bassetsnn  13258  gsumfzz  13697  gsumfzcl  13701  gsumfzreidx  14043  gsumfzsubmcl  14044  gsumfzmptfidmadd  14045  gsumfzmhm  14049  gsumfzfsum  14723  znf1o  14786  lgslem4  15863  lgsneg  15884  lgsmod  15886  lgsdilem  15887  lgsdir2  15893  lgsdir  15895  lgsdi  15897  lgsne0  15898  lgsdirnn0  15907  lgsdinn0  15908  gausslemma2dlem1a  15918  gausslemma2dlem1f1o  15920  lgsquadlem2  15938  lgsquad3  15944  2lgs  15964  umgrclwwlkge2  16384  eupth2lem3lem4fi  16455  eupth2lem3lem7fi  16456  sumdc2  16558  nnsf  16770  nninfsellemsuc  16777  nninffeq  16785  apdifflemr  16818  nconstwlpolem  16837  gsumgfsum  16852