Theorem exmiddc 841

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 713  DECID wdc 839

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 840

This theorem is referenced by:  stdcndcOLD  851  dfifp2dc  987  ifpiddc  997  modc  2121  rabxmdc  3523  dcun  3601  ifsbdc  3615  ifcldadc  3632  ifeq1dadc  3633  ifeq2dadc  3634  ifeqdadc  3635  ifbothdadc  3636  ifbothdc  3637  ifiddc  3638  eqifdc  3639  2if2dc  3642  ifordc  3644  exmid1dc  4285  exmidn0m  4286  exmidundif  4291  exmidundifim  4292  dcextest  4674  dcdifsnid  6663  pw2f1odclem  7008  fidceq  7044  fidifsnen  7045  fidcen  7074  fimax2gtrilemstep  7076  finexdc  7078  elssdc  7080  eqsndc  7081  unfiexmid  7096  unsnfidcex  7098  unsnfidcel  7099  undifdcss  7101  prfidceq  7106  tpfidceq  7108  ssfirab  7114  fidcenumlemrks  7136  omp1eomlem  7277  difinfsnlem  7282  difinfsn  7283  ctssdc  7296  nnnninf  7309  nnnninfeq2  7312  nninfisol  7316  exmidomniim  7324  nninfwlpoimlemg  7358  exmidfodomrlemim  7395  netap  7456  2omotaplemap  7459  xaddcom  10074  xnegdi  10081  xpncan  10084  xleadd1a  10086  xsubge0  10094  exfzdc  10463  zsupcllemstep  10466  infssuzex  10470  flqeqceilz  10557  modifeq2int  10625  modfzo0difsn  10634  modsumfzodifsn  10635  iseqf1olemab  10741  iseqf1olemmo  10744  seq3f1olemstep  10753  seqf1oglem1  10758  fser0const  10774  bcval  10988  bccmpl  10993  bcval5  11002  bcpasc  11005  bccl  11006  hashfzp1  11064  ccatsymb  11155  fzowrddc  11200  swrd0g  11213  swrdsbslen  11219  swrdspsleq  11220  pfxclz  11232  pfxccatin12  11286  swrdccat  11288  pfxccat3a  11291  swrdccat3blem  11292  2zsupmax  11758  2zinfmin  11775  xrmaxifle  11778  xrmaxiflemab  11779  xrmaxiflemlub  11780  xrmaxiflemcom  11781  sumdc  11890  sumrbdclem  11909  fsum3cvg  11910  summodclem2a  11913  zsumdc  11916  isumss  11923  fisumss  11924  isumss2  11925  fsumadd  11938  sumsplitdc  11964  fsummulc2  11980  prodrbdclem  12103  fproddccvg  12104  zproddc  12111  prod1dc  12118  prodssdc  12121  fprodssdc  12122  fprodmul  12123  fprodsplitdc  12128  dvdsabseq  12379  bitsmod  12488  gcdval  12501  gcddvds  12505  gcdcl  12508  gcd0id  12521  gcdneg  12524  gcdaddm  12526  dfgcd3  12552  dfgcd2  12556  gcdmultiplez  12563  dvdssq  12573  dvdslcm  12612  lcmcl  12615  lcmneg  12617  lcmgcd  12621  lcmdvds  12622  lcmid  12623  mulgcddvds  12637  cncongr2  12647  prmind2  12663  rpexp  12696  pw2dvdslemn  12708  fermltl  12777  pclemdc  12832  pcxcl  12855  pcgcd  12873  pcmptcl  12886  pcmpt  12887  pcmpt2  12888  pcprod  12890  fldivp1  12892  1arith  12911  unennn  12989  ennnfonelemss  13002  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ctiunctlemudc  13029  bassetsnn  13110  gsumfzz  13549  gsumfzcl  13553  gsumfzreidx  13895  gsumfzsubmcl  13896  gsumfzmptfidmadd  13897  gsumfzmhm  13901  gsumfzfsum  14573  znf1o  14636  lgslem4  15703  lgsneg  15724  lgsmod  15726  lgsdilem  15727  lgsdir2  15733  lgsdir  15735  lgsdi  15737  lgsne0  15738  lgsdirnn0  15747  lgsdinn0  15748  gausslemma2dlem1a  15758  gausslemma2dlem1f1o  15760  lgsquadlem2  15778  lgsquad3  15784  2lgs  15804  umgrclwwlkge2  16171  sumdc2  16272  2omap  16472  nnsf  16485  nninfsellemsuc  16492  nninffeq  16500  apdifflemr  16529  nconstwlpolem  16547