Theorem exmiddc 843

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 715  DECID wdc 841

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 842

This theorem is referenced by:  stdcndcOLD  853  dfifp2dc  989  ifpiddc  999  modc  2123  rabxmdc  3526  dcun  3604  ifsbdc  3618  ifcldadc  3635  ifeq1dadc  3636  ifeq2dadc  3637  ifeqdadc  3638  ifbothdadc  3639  ifbothdc  3640  ifiddc  3641  eqifdc  3642  2if2dc  3645  ifordc  3647  exmid1dc  4290  exmidn0m  4291  exmidundif  4296  exmidundifim  4297  dcextest  4679  dcdifsnid  6672  pw2f1odclem  7020  fidceq  7056  fidifsnen  7057  fidcen  7088  fimax2gtrilemstep  7090  finexdc  7092  elssdc  7094  eqsndc  7095  unfiexmid  7110  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  prfidceq  7120  tpfidceq  7122  ssfirab  7129  fidcenumlemrks  7152  omp1eomlem  7293  difinfsnlem  7298  difinfsn  7299  ctssdc  7312  nnnninf  7325  nnnninfeq2  7328  nninfisol  7332  exmidomniim  7340  nninfwlpoimlemg  7374  exmidfodomrlemim  7412  netap  7473  2omotaplemap  7476  xaddcom  10096  xnegdi  10103  xpncan  10106  xleadd1a  10108  xsubge0  10116  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  flqeqceilz  10581  modifeq2int  10649  modfzo0difsn  10658  modsumfzodifsn  10659  iseqf1olemab  10765  iseqf1olemmo  10768  seq3f1olemstep  10777  seqf1oglem1  10782  fser0const  10798  bcval  11012  bccmpl  11017  bcval5  11026  bcpasc  11029  bccl  11030  hashfzp1  11089  ccatsymb  11180  fzowrddc  11229  swrd0g  11242  swrdsbslen  11248  swrdspsleq  11249  pfxclz  11261  pfxccatin12  11315  swrdccat  11317  pfxccat3a  11320  swrdccat3blem  11321  2zsupmax  11788  2zinfmin  11805  xrmaxifle  11808  xrmaxiflemab  11809  xrmaxiflemlub  11810  xrmaxiflemcom  11811  sumdc  11920  sumrbdclem  11940  fsum3cvg  11941  summodclem2a  11944  zsumdc  11947  isumss  11954  fisumss  11955  isumss2  11956  fsumadd  11969  sumsplitdc  11995  fsummulc2  12011  prodrbdclem  12134  fproddccvg  12135  zproddc  12142  prod1dc  12149  prodssdc  12152  fprodssdc  12153  fprodmul  12154  fprodsplitdc  12159  dvdsabseq  12410  bitsmod  12519  gcdval  12532  gcddvds  12536  gcdcl  12539  gcd0id  12552  gcdneg  12555  gcdaddm  12557  dfgcd3  12583  dfgcd2  12587  gcdmultiplez  12594  dvdssq  12604  dvdslcm  12643  lcmcl  12646  lcmneg  12648  lcmgcd  12652  lcmdvds  12653  lcmid  12654  mulgcddvds  12668  cncongr2  12678  prmind2  12694  rpexp  12727  pw2dvdslemn  12739  fermltl  12808  pclemdc  12863  pcxcl  12886  pcgcd  12904  pcmptcl  12917  pcmpt  12918  pcmpt2  12919  pcprod  12921  fldivp1  12923  1arith  12942  unennn  13020  ennnfonelemss  13033  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ctiunctlemudc  13060  bassetsnn  13141  gsumfzz  13580  gsumfzcl  13584  gsumfzreidx  13926  gsumfzsubmcl  13927  gsumfzmptfidmadd  13928  gsumfzmhm  13932  gsumfzfsum  14605  znf1o  14668  lgslem4  15735  lgsneg  15756  lgsmod  15758  lgsdilem  15759  lgsdir2  15765  lgsdir  15767  lgsdi  15769  lgsne0  15770  lgsdirnn0  15779  lgsdinn0  15780  gausslemma2dlem1a  15790  gausslemma2dlem1f1o  15792  lgsquadlem2  15810  lgsquad3  15816  2lgs  15836  umgrclwwlkge2  16256  eupth2lem3lem4fi  16327  eupth2lem3lem7fi  16328  sumdc2  16416  2omap  16615  nnsf  16628  nninfsellemsuc  16635  nninffeq  16643  apdifflemr  16672  nconstwlpolem  16690  gsumgfsum  16705