Theorem exmiddc 837

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 709  DECID wdc 835

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 836

This theorem is referenced by:  stdcndcOLD  847  modc  2088  rabxmdc  3483  dcun  3561  ifsbdc  3574  ifcldadc  3591  ifeq1dadc  3592  ifeq2dadc  3593  ifbothdadc  3594  ifbothdc  3595  ifiddc  3596  eqifdc  3597  ifordc  3601  exmid1dc  4234  exmidn0m  4235  exmidundif  4240  exmidundifim  4241  dcextest  4618  dcdifsnid  6571  pw2f1odclem  6904  fidceq  6939  fidifsnen  6940  fimax2gtrilemstep  6970  finexdc  6972  unfiexmid  6988  unsnfidcex  6990  unsnfidcel  6991  undifdcss  6993  prfidceq  6998  tpfidceq  7000  ssfirab  7006  fidcenumlemrks  7028  omp1eomlem  7169  difinfsnlem  7174  difinfsn  7175  ctssdc  7188  nnnninf  7201  nnnninfeq2  7204  nninfisol  7208  exmidomniim  7216  nninfwlpoimlemg  7250  exmidfodomrlemim  7282  netap  7339  2omotaplemap  7342  xaddcom  9955  xnegdi  9962  xpncan  9965  xleadd1a  9967  xsubge0  9975  exfzdc  10335  zsupcllemstep  10338  infssuzex  10342  flqeqceilz  10429  modifeq2int  10497  modfzo0difsn  10506  modsumfzodifsn  10507  iseqf1olemab  10613  iseqf1olemmo  10616  seq3f1olemstep  10625  seqf1oglem1  10630  fser0const  10646  bcval  10860  bccmpl  10865  bcval5  10874  bcpasc  10877  bccl  10878  hashfzp1  10935  2zsupmax  11410  2zinfmin  11427  xrmaxifle  11430  xrmaxiflemab  11431  xrmaxiflemlub  11432  xrmaxiflemcom  11433  sumdc  11542  sumrbdclem  11561  fsum3cvg  11562  summodclem2a  11565  zsumdc  11568  isumss  11575  fisumss  11576  isumss2  11577  fsumadd  11590  sumsplitdc  11616  fsummulc2  11632  prodrbdclem  11755  fproddccvg  11756  zproddc  11763  prod1dc  11770  prodssdc  11773  fprodssdc  11774  fprodmul  11775  fprodsplitdc  11780  dvdsabseq  12031  bitsmod  12140  gcdval  12153  gcddvds  12157  gcdcl  12160  gcd0id  12173  gcdneg  12176  gcdaddm  12178  dfgcd3  12204  dfgcd2  12208  gcdmultiplez  12215  dvdssq  12225  dvdslcm  12264  lcmcl  12267  lcmneg  12269  lcmgcd  12273  lcmdvds  12274  lcmid  12275  mulgcddvds  12289  cncongr2  12299  prmind2  12315  rpexp  12348  pw2dvdslemn  12360  fermltl  12429  pclemdc  12484  pcxcl  12507  pcgcd  12525  pcmptcl  12538  pcmpt  12539  pcmpt2  12540  pcprod  12542  fldivp1  12544  1arith  12563  unennn  12641  ennnfonelemss  12654  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ctiunctlemudc  12681  gsumfzz  13199  gsumfzcl  13203  gsumfzreidx  13545  gsumfzsubmcl  13546  gsumfzmptfidmadd  13547  gsumfzmhm  13551  gsumfzfsum  14222  znf1o  14285  lgslem4  15352  lgsneg  15373  lgsmod  15375  lgsdilem  15376  lgsdir2  15382  lgsdir  15384  lgsdi  15386  lgsne0  15387  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  lgsquadlem2  15427  lgsquad3  15433  2lgs  15453  sumdc2  15553  2omap  15750  nnsf  15760  nninfsellemsuc  15767  nninffeq  15775  apdifflemr  15804  nconstwlpolem  15822