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  4339  exmidn0m  4340  exmidundif  4345  exmidundifim  4346  dcextest  4730  dcdifsnid  6781  pw2f1odclem  7139  fidceq  7176  fidifsnen  7177  fidcen  7208  fimax2gtrilemstep  7210  finexdc  7212  elssdc  7214  eqsndc  7215  unfiexmid  7230  unsnfidcex  7232  unsnfidcel  7233  undifdcss  7235  prfidceq  7240  tpfidceq  7242  ssfirab  7249  fidcenumlemrks  7276  2omap  7325  omp1eomlem  7441  difinfsnlem  7446  difinfsn  7447  ctssdc  7460  nnnninf  7473  nnnninfeq2  7476  nninfisol  7480  exmidomniim  7488  nninfwlpoimlemg  7522  exmidfodomrlemim  7560  netap  7627  2omotaplemap  7630  xaddcom  10281  xnegdi  10288  xpncan  10291  xleadd1a  10293  xsubge0  10301  exfzdc  10677  zsupcllemstep  10680  infssuzex  10684  flqeqceilz  10777  modifeq2int  10845  modfzo0difsn  10854  modsumfzodifsn  10855  iseqf1olemab  10961  iseqf1olemmo  10964  seq3f1olemstep  10973  seqf1oglem1  10978  fser0const  10994  bcval  11210  bccmpl  11215  bcval5  11224  bcpasc  11227  bccl  11228  hashfzp1  11288  hashfibc  11306  ccatsymb  11393  fzowrddc  11442  swrd0g  11455  swrdsbslen  11461  swrdspsleq  11462  pfxclz  11474  pfxccatin12  11528  swrdccat  11530  pfxccat3a  11533  swrdccat3blem  11534  2zsupmax  12016  2zinfmin  12035  xrmaxifle  12038  xrmaxiflemab  12039  xrmaxiflemlub  12040  xrmaxiflemcom  12041  sumdc  12150  sumrbdclem  12170  fsum3cvg  12171  summodclem2a  12174  zsumdc  12177  isumss  12184  fisumss  12185  isumss2  12186  fsumadd  12199  sumsplitdc  12225  fsummulc2  12241  prodrbdclem  12364  fproddccvg  12365  zproddc  12372  prod1dc  12379  prodssdc  12382  fprodssdc  12383  fprodmul  12384  fprodsplitdc  12389  dvdsabseq  12640  bitsmod  12749  gcdval  12762  gcddvds  12766  gcdcl  12769  gcd0id  12782  gcdneg  12785  gcdaddm  12787  dfgcd3  12813  dfgcd2  12817  gcdmultiplez  12824  dvdssq  12834  dvdslcm  12873  lcmcl  12876  lcmneg  12878  lcmgcd  12882  lcmdvds  12883  lcmid  12884  mulgcddvds  12898  cncongr2  12908  prmind2  12924  prmdcz  12935  rpexp  12958  pwbdvdslemn  12970  nn0sqdcq  13014  sqrtrirr  13015  fermltl  13042  pclemdc  13097  pcxcl  13120  pcgcd  13138  pcmptcl  13151  pcmpt  13152  pcmpt2  13153  pcprod  13155  fldivp1  13157  1arith  13176  unennn  13347  ennnfonelemss  13360  ennnfonelemkh  13362  ennnfonelemhf1o  13363  ctiunctlemudc  13387  bassetsnn  13468  gzsumcl  13864  gzsumreidx  14232  gzsumsubmcl  14233  gzsummhm  14236  gzsumgsum  14246  gsumresfi  14264  znf1o  15096  ppiqp1le  16279  chtublem  16307  bposlem1  16323  bposlem3  16325  bposlem5  16327  bposlem6  16328  lgslem4  16339  lgsneg  16360  lgsmod  16362  lgsdilem  16363  lgsdir2  16369  lgsdir  16371  lgsdi  16373  lgsne0  16374  lgsdirnn0  16383  lgsdinn0  16384  gausslemma2dlem1a  16394  gausslemma2dlem1f1o  16396  lgsquadlem2  16414  lgsquad3  16420  2lgs  16440  umgrclwwlkge2  16860  eupth2lem3lem4fi  16931  eupth2lem3lem7fi  16932  sumdc2  17044  wexmiddifxy  17263  nnsf  17266  nninfsellemsuc  17273  nninffeq  17281  apdifflemr  17315  nconstwlpolem  17334