Theorem exmiddc 848

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 720  DECID wdc 846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-dc 847

This theorem is used by:  stdcndcOLD  858  dfifp2dc  994  ifpiddc  1004  modc  2130  rabxmdc  3554  dcun  3637  ifsbdc  3653  ifcldadc  3670  ifeq1dadc  3671  ifeq2dadc  3672  ifeqdadc  3673  ifbothdadc  3674  ifbothdc  3675  ifiddc  3676  eqifdc  3677  2if2dc  3680  ifordc  3682  ifeqeqxdc  3687  exmid1dc  4337  exmidn0m  4338  exmidundif  4343  exmidundifim  4344  dcextest  4728  dcdifsnid  6777  pw2f1odclem  7134  fidceq  7171  fidifsnen  7172  fidcen  7203  fimax2gtrilemstep  7205  finexdc  7207  elssdc  7209  eqsndc  7210  unfiexmid  7225  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  prfidceq  7235  tpfidceq  7237  ssfirab  7244  fidcenumlemrks  7270  2omap  7318  omp1eomlem  7434  difinfsnlem  7439  difinfsn  7440  ctssdc  7453  nnnninf  7466  nnnninfeq2  7469  nninfisol  7473  exmidomniim  7481  nninfwlpoimlemg  7515  exmidfodomrlemim  7553  netap  7620  2omotaplemap  7623  xaddcom  10265  xnegdi  10272  xpncan  10275  xleadd1a  10277  xsubge0  10285  exfzdc  10661  zsupcllemstep  10664  infssuzex  10668  flqeqceilz  10757  modifeq2int  10825  modfzo0difsn  10834  modsumfzodifsn  10835  iseqf1olemab  10941  iseqf1olemmo  10944  seq3f1olemstep  10953  seqf1oglem1  10958  fser0const  10974  bcval  11189  bccmpl  11194  bcval5  11203  bcpasc  11206  bccl  11207  hashfzp1  11267  hashfibc  11285  ccatsymb  11372  fzowrddc  11421  swrd0g  11434  swrdsbslen  11440  swrdspsleq  11441  pfxclz  11453  pfxccatin12  11507  swrdccat  11509  pfxccat3a  11512  swrdccat3blem  11513  2zsupmax  11994  2zinfmin  12011  xrmaxifle  12014  xrmaxiflemab  12015  xrmaxiflemlub  12016  xrmaxiflemcom  12017  sumdc  12126  sumrbdclem  12146  fsum3cvg  12147  summodclem2a  12150  zsumdc  12153  isumss  12160  fisumss  12161  isumss2  12162  fsumadd  12175  sumsplitdc  12201  fsummulc2  12217  prodrbdclem  12340  fproddccvg  12341  zproddc  12348  prod1dc  12355  prodssdc  12358  fprodssdc  12359  fprodmul  12360  fprodsplitdc  12365  dvdsabseq  12616  bitsmod  12725  gcdval  12738  gcddvds  12742  gcdcl  12745  gcd0id  12758  gcdneg  12761  gcdaddm  12763  dfgcd3  12789  dfgcd2  12793  gcdmultiplez  12800  dvdssq  12810  dvdslcm  12849  lcmcl  12852  lcmneg  12854  lcmgcd  12858  lcmdvds  12859  lcmid  12860  mulgcddvds  12874  cncongr2  12884  prmind2  12900  rpexp  12933  pw2dvdslemn  12945  fermltl  13014  pclemdc  13069  pcxcl  13092  pcgcd  13110  pcmptcl  13123  pcmpt  13124  pcmpt2  13125  pcprod  13127  fldivp1  13129  1arith  13148  unennn  13290  ennnfonelemss  13303  ennnfonelemkh  13305  ennnfonelemhf1o  13306  ctiunctlemudc  13330  bassetsnn  13411  gzsumcl  13806  gzsumreidx  14143  gzsumsubmcl  14144  gzsummhm  14147  gzsumgsum  14157  znf1o  14988  lgslem4  16134  lgsneg  16155  lgsmod  16157  lgsdilem  16158  lgsdir2  16164  lgsdir  16166  lgsdi  16168  lgsne0  16169  lgsdirnn0  16178  lgsdinn0  16179  gausslemma2dlem1a  16189  gausslemma2dlem1f1o  16191  lgsquadlem2  16209  lgsquad3  16215  2lgs  16235  umgrclwwlkge2  16655  eupth2lem3lem4fi  16726  eupth2lem3lem7fi  16727  sumdc2  16839  wexmiddifxy  17058  nnsf  17060  nninfsellemsuc  17067  nninffeq  17075  apdifflemr  17108  nconstwlpolem  17127