Theorem exmiddc 826

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

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

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 825

This theorem is referenced by:  stdcndcOLD  836  modc  2057  rabxmdc  3439  dcun  3518  ifsbdc  3531  ifcldadc  3548  ifeq1dadc  3549  ifbothdadc  3550  ifbothdc  3551  ifiddc  3552  eqifdc  3553  exmid1dc  4178  exmidn0m  4179  exmidundif  4184  exmidundifim  4185  dcextest  4557  dcdifsnid  6468  fidceq  6831  fidifsnen  6832  fimax2gtrilemstep  6862  finexdc  6864  unfiexmid  6879  unsnfidcex  6881  unsnfidcel  6882  undifdcss  6884  ssfirab  6895  fidcenumlemrks  6914  omp1eomlem  7055  difinfsnlem  7060  difinfsn  7061  ctssdc  7074  nnnninf  7086  nnnninfeq2  7089  nninfisol  7093  exmidomniim  7101  exmidfodomrlemim  7153  xaddcom  9793  xnegdi  9800  xpncan  9803  xleadd1a  9805  xsubge0  9813  exfzdc  10171  flqeqceilz  10249  modifeq2int  10317  modfzo0difsn  10326  modsumfzodifsn  10327  iseqf1olemab  10420  iseqf1olemmo  10423  seq3f1olemstep  10432  fser0const  10447  bcval  10658  bccmpl  10663  bcval5  10672  bcpasc  10675  bccl  10676  hashfzp1  10733  2zsupmax  11163  2zinfmin  11180  xrmaxifle  11183  xrmaxiflemab  11184  xrmaxiflemlub  11185  xrmaxiflemcom  11186  sumdc  11295  sumrbdclem  11314  fsum3cvg  11315  summodclem2a  11318  zsumdc  11321  isumss  11328  fisumss  11329  isumss2  11330  fsumadd  11343  sumsplitdc  11369  fsummulc2  11385  prodrbdclem  11508  fproddccvg  11509  zproddc  11516  prod1dc  11523  prodssdc  11526  fprodssdc  11527  fprodmul  11528  fprodsplitdc  11533  dvdsabseq  11781  zsupcllemstep  11874  infssuzex  11878  gcdval  11888  gcddvds  11892  gcdcl  11895  gcd0id  11908  gcdneg  11911  gcdaddm  11913  dfgcd3  11939  dfgcd2  11943  gcdmultiplez  11950  dvdssq  11960  dvdslcm  11997  lcmcl  12000  lcmneg  12002  lcmgcd  12006  lcmdvds  12007  lcmid  12008  mulgcddvds  12022  cncongr2  12032  prmind2  12048  rpexp  12081  pw2dvdslemn  12093  fermltl  12162  pclemdc  12216  pcxcl  12239  pcgcd  12256  pcmptcl  12268  pcmpt  12269  pcmpt2  12270  pcprod  12272  fldivp1  12274  1arith  12293  unennn  12326  ennnfonelemss  12339  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ctiunctlemudc  12366  lgslem4  13504  lgsneg  13525  lgsmod  13527  lgsdilem  13528  lgsdir2  13534  lgsdir  13536  lgsdi  13538  lgsne0  13539  lgsdirnn0  13548  lgsdinn0  13549  sumdc2  13640  nnsf  13845  nninfsellemsuc  13852  nninffeq  13860  apdifflemr  13886  nconstwlpolem  13903