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  10273  xnegdi  10280  xpncan  10283  xleadd1a  10285  xsubge0  10293  exfzdc  10669  zsupcllemstep  10672  infssuzex  10676  flqeqceilz  10768  modifeq2int  10836  modfzo0difsn  10845  modsumfzodifsn  10846  iseqf1olemab  10952  iseqf1olemmo  10955  seq3f1olemstep  10964  seqf1oglem1  10969  fser0const  10985  bcval  11201  bccmpl  11206  bcval5  11215  bcpasc  11218  bccl  11219  hashfzp1  11279  hashfibc  11297  ccatsymb  11384  fzowrddc  11433  swrd0g  11446  swrdsbslen  11452  swrdspsleq  11453  pfxclz  11465  pfxccatin12  11519  swrdccat  11521  pfxccat3a  11524  swrdccat3blem  11525  2zsupmax  12007  2zinfmin  12025  xrmaxifle  12028  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxiflemcom  12031  sumdc  12140  sumrbdclem  12160  fsum3cvg  12161  summodclem2a  12164  zsumdc  12167  isumss  12174  fisumss  12175  isumss2  12176  fsumadd  12189  sumsplitdc  12215  fsummulc2  12231  prodrbdclem  12354  fproddccvg  12355  zproddc  12362  prod1dc  12369  prodssdc  12372  fprodssdc  12373  fprodmul  12374  fprodsplitdc  12379  dvdsabseq  12630  bitsmod  12739  gcdval  12752  gcddvds  12756  gcdcl  12759  gcd0id  12772  gcdneg  12775  gcdaddm  12777  dfgcd3  12803  dfgcd2  12807  gcdmultiplez  12814  dvdssq  12824  dvdslcm  12863  lcmcl  12866  lcmneg  12868  lcmgcd  12872  lcmdvds  12873  lcmid  12874  mulgcddvds  12888  cncongr2  12898  prmind2  12914  prmdcz  12925  rpexp  12948  pwbdvdslemn  12960  nn0sqdcq  13004  sqrtrirr  13005  fermltl  13032  pclemdc  13087  pcxcl  13110  pcgcd  13128  pcmptcl  13141  pcmpt  13142  pcmpt2  13143  pcprod  13145  fldivp1  13147  1arith  13166  unennn  13337  ennnfonelemss  13350  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ctiunctlemudc  13377  bassetsnn  13458  gzsumcl  13853  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  gzsumgsum  14204  znf1o  15035  ppiqp1le  16186  chtublem  16214  bposlem1  16230  bposlem3  16232  bposlem5  16234  lgslem4  16241  lgsneg  16262  lgsmod  16264  lgsdilem  16265  lgsdir2  16271  lgsdir  16273  lgsdi  16275  lgsne0  16276  lgsdirnn0  16285  lgsdinn0  16286  gausslemma2dlem1a  16296  gausslemma2dlem1f1o  16298  lgsquadlem2  16316  lgsquad3  16322  2lgs  16342  umgrclwwlkge2  16762  eupth2lem3lem4fi  16833  eupth2lem3lem7fi  16834  sumdc2  16946  wexmiddifxy  17165  nnsf  17167  nninfsellemsuc  17174  nninffeq  17182  apdifflemr  17215  nconstwlpolem  17234