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  2043  rabxmdc  3399  dcun  3478  ifsbdc  3491  ifcldadc  3506  ifeq1dadc  3507  ifbothdadc  3508  ifbothdc  3509  ifiddc  3510  eqifdc  3511  exmid1dc  4131  exmidn0m  4132  exmidundif  4137  exmidundifim  4138  dcextest  4503  dcdifsnid  6408  fidceq  6771  fidifsnen  6772  fimax2gtrilemstep  6802  finexdc  6804  unfiexmid  6814  unsnfidcex  6816  unsnfidcel  6817  undifdcss  6819  ssfirab  6830  fidcenumlemrks  6849  omp1eomlem  6987  difinfsnlem  6992  difinfsn  6993  ctssdc  7006  exmidomniim  7021  nnnninf  7031  exmidfodomrlemim  7074  xaddcom  9674  xnegdi  9681  xpncan  9684  xleadd1a  9686  xsubge0  9694  exfzdc  10048  flqeqceilz  10122  modifeq2int  10190  modfzo0difsn  10199  modsumfzodifsn  10200  iseqf1olemab  10293  iseqf1olemmo  10296  seq3f1olemstep  10305  fser0const  10320  bcval  10527  bccmpl  10532  bcval5  10541  bcpasc  10544  bccl  10545  hashfzp1  10602  2zsupmax  11029  xrmaxifle  11047  xrmaxiflemab  11048  xrmaxiflemlub  11049  xrmaxiflemcom  11050  sumdc  11159  sumrbdclem  11178  fsum3cvg  11179  summodclem2a  11182  zsumdc  11185  isumss  11192  fisumss  11193  isumss2  11194  fsumadd  11207  sumsplitdc  11233  fsummulc2  11249  prodrbdclem  11372  fproddccvg  11373  zproddc  11380  dvdsabseq  11581  zsupcllemstep  11674  infssuzex  11678  gcdval  11684  gcddvds  11688  gcdcl  11691  gcd0id  11703  gcdneg  11706  gcdaddm  11708  dfgcd3  11734  dfgcd2  11738  gcdmultiplez  11745  dvdssq  11755  dvdslcm  11786  lcmcl  11789  lcmneg  11791  lcmgcd  11795  lcmdvds  11796  lcmid  11797  mulgcddvds  11811  cncongr2  11821  prmind2  11837  rpexp  11867  pw2dvdslemn  11879  unennn  11946  ennnfonelemss  11959  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ctiunctlemudc  11986  sumdc2  13177  nnsf  13374  nninfsellemsuc  13383  nninffeq  13391  apdifflemr  13415