Theorem exmiddc 822

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 698  DECID wdc 820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-dc 821

This theorem is referenced by:  stdcndcOLD  832  modc  2049  rabxmdc  3425  dcun  3504  ifsbdc  3517  ifcldadc  3534  ifeq1dadc  3535  ifbothdadc  3536  ifbothdc  3537  ifiddc  3538  eqifdc  3539  exmid1dc  4162  exmidn0m  4163  exmidundif  4168  exmidundifim  4169  dcextest  4541  dcdifsnid  6452  fidceq  6815  fidifsnen  6816  fimax2gtrilemstep  6846  finexdc  6848  unfiexmid  6863  unsnfidcex  6865  unsnfidcel  6866  undifdcss  6868  ssfirab  6879  fidcenumlemrks  6898  omp1eomlem  7039  difinfsnlem  7044  difinfsn  7045  ctssdc  7058  nnnninf  7070  nnnninfeq2  7073  nninfisol  7077  exmidomniim  7085  exmidfodomrlemim  7137  xaddcom  9766  xnegdi  9773  xpncan  9776  xleadd1a  9778  xsubge0  9786  exfzdc  10143  flqeqceilz  10221  modifeq2int  10289  modfzo0difsn  10298  modsumfzodifsn  10299  iseqf1olemab  10392  iseqf1olemmo  10395  seq3f1olemstep  10404  fser0const  10419  bcval  10627  bccmpl  10632  bcval5  10641  bcpasc  10644  bccl  10645  hashfzp1  10702  2zsupmax  11129  xrmaxifle  11147  xrmaxiflemab  11148  xrmaxiflemlub  11149  xrmaxiflemcom  11150  sumdc  11259  sumrbdclem  11278  fsum3cvg  11279  summodclem2a  11282  zsumdc  11285  isumss  11292  fisumss  11293  isumss2  11294  fsumadd  11307  sumsplitdc  11333  fsummulc2  11349  prodrbdclem  11472  fproddccvg  11473  zproddc  11480  prod1dc  11487  prodssdc  11490  fprodssdc  11491  fprodmul  11492  fprodsplitdc  11497  dvdsabseq  11743  zsupcllemstep  11836  infssuzex  11840  gcdval  11847  gcddvds  11851  gcdcl  11854  gcd0id  11867  gcdneg  11870  gcdaddm  11872  dfgcd3  11898  dfgcd2  11902  gcdmultiplez  11909  dvdssq  11919  dvdslcm  11950  lcmcl  11953  lcmneg  11955  lcmgcd  11959  lcmdvds  11960  lcmid  11961  mulgcddvds  11975  cncongr2  11985  prmind2  12001  rpexp  12032  pw2dvdslemn  12044  fermltl  12113  unennn  12168  ennnfonelemss  12181  ennnfonelemkh  12183  ennnfonelemhf1o  12184  ctiunctlemudc  12208  sumdc2  13415  nnsf  13619  nninfsellemsuc  13626  nninffeq  13634  apdifflemr  13660  nconstwlpolem  13677