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 𝜑 → (𝜑 ∨ ¬ 𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 720  DECID wdc 846

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

This theorem depends on definitions:  df-bi 117  df-dc 847

This theorem is referenced 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  4335  exmidn0m  4336  exmidundif  4341  exmidundifim  4342  dcextest  4726  dcdifsnid  6771  pw2f1odclem  7128  fidceq  7165  fidifsnen  7166  fidcen  7197  fimax2gtrilemstep  7199  finexdc  7201  elssdc  7203  eqsndc  7204  unfiexmid  7219  unsnfidcex  7221  unsnfidcel  7222  undifdcss  7224  prfidceq  7229  tpfidceq  7231  ssfirab  7238  fidcenumlemrks  7264  2omap  7312  omp1eomlem  7428  difinfsnlem  7433  difinfsn  7434  ctssdc  7447  nnnninf  7460  nnnninfeq2  7463  nninfisol  7467  exmidomniim  7475  nninfwlpoimlemg  7509  exmidfodomrlemim  7547  netap  7614  2omotaplemap  7617  xaddcom  10246  xnegdi  10253  xpncan  10256  xleadd1a  10258  xsubge0  10266  exfzdc  10642  zsupcllemstep  10645  infssuzex  10649  flqeqceilz  10738  modifeq2int  10806  modfzo0difsn  10815  modsumfzodifsn  10816  iseqf1olemab  10922  iseqf1olemmo  10925  seq3f1olemstep  10934  seqf1oglem1  10939  fser0const  10955  bcval  11170  bccmpl  11175  bcval5  11184  bcpasc  11187  bccl  11188  hashfzp1  11248  hashfibc  11266  ccatsymb  11353  fzowrddc  11402  swrd0g  11415  swrdsbslen  11421  swrdspsleq  11422  pfxclz  11434  pfxccatin12  11488  swrdccat  11490  pfxccat3a  11493  swrdccat3blem  11494  2zsupmax  11975  2zinfmin  11992  xrmaxifle  11995  xrmaxiflemab  11996  xrmaxiflemlub  11997  xrmaxiflemcom  11998  sumdc  12107  sumrbdclem  12127  fsum3cvg  12128  summodclem2a  12131  zsumdc  12134  isumss  12141  fisumss  12142  isumss2  12143  fsumadd  12156  sumsplitdc  12182  fsummulc2  12198  prodrbdclem  12321  fproddccvg  12322  zproddc  12329  prod1dc  12336  prodssdc  12339  fprodssdc  12340  fprodmul  12341  fprodsplitdc  12346  dvdsabseq  12597  bitsmod  12706  gcdval  12719  gcddvds  12723  gcdcl  12726  gcd0id  12739  gcdneg  12742  gcdaddm  12744  dfgcd3  12770  dfgcd2  12774  gcdmultiplez  12781  dvdssq  12791  dvdslcm  12830  lcmcl  12833  lcmneg  12835  lcmgcd  12839  lcmdvds  12840  lcmid  12841  mulgcddvds  12855  cncongr2  12865  prmind2  12881  rpexp  12914  pw2dvdslemn  12926  fermltl  12995  pclemdc  13050  pcxcl  13073  pcgcd  13091  pcmptcl  13104  pcmpt  13105  pcmpt2  13106  pcprod  13108  fldivp1  13110  1arith  13129  unennn  13271  ennnfonelemss  13284  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ctiunctlemudc  13311  bassetsnn  13392  gzsumcl  13787  gzsumreidx  14124  gzsumsubmcl  14125  gzsummhm  14128  gzsumgsum  14138  znf1o  14969  lgslem4  16105  lgsneg  16126  lgsmod  16128  lgsdilem  16129  lgsdir2  16135  lgsdir  16137  lgsdi  16139  lgsne0  16140  lgsdirnn0  16149  lgsdinn0  16150  gausslemma2dlem1a  16160  gausslemma2dlem1f1o  16162  lgsquadlem2  16180  lgsquad3  16186  2lgs  16206  umgrclwwlkge2  16626  eupth2lem3lem4fi  16697  eupth2lem3lem7fi  16698  sumdc2  16810  nnsf  17022  nninfsellemsuc  17029  nninffeq  17037  apdifflemr  17070  nconstwlpolem  17089