Theorem exmiddc 844

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 ph -> ( ph \/ -. ph ) )

Proof of Theorem exmiddc

Step	Hyp	Ref	Expression
1		df-dc 843	. 2 |- (DECID ph <-> ( ph \/ -. ph ) )
2	1	biimpi 120	1 |- (DECID ph -> ( ph \/ -. ph ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 716  DECID wdc 842

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 843

This theorem is referenced by:  stdcndcOLD  854  dfifp2dc  990  ifpiddc  1000  modc  2126  rabxmdc  3544  dcun  3623  ifsbdc  3639  ifcldadc  3656  ifeq1dadc  3657  ifeq2dadc  3658  ifeqdadc  3659  ifbothdadc  3660  ifbothdc  3661  ifiddc  3662  eqifdc  3663  2if2dc  3666  ifordc  3668  ifeqeqxdc  3673  exmid1dc  4318  exmidn0m  4319  exmidundif  4324  exmidundifim  4325  dcextest  4708  dcdifsnid  6750  pw2f1odclem  7100  fidceq  7137  fidifsnen  7138  fidcen  7169  fimax2gtrilemstep  7171  finexdc  7173  elssdc  7175  eqsndc  7176  unfiexmid  7191  unsnfidcex  7193  unsnfidcel  7194  undifdcss  7196  prfidceq  7201  tpfidceq  7203  ssfirab  7210  fidcenumlemrks  7236  2omap  7282  omp1eomlem  7398  difinfsnlem  7403  difinfsn  7404  ctssdc  7417  nnnninf  7430  nnnninfeq2  7433  nninfisol  7437  exmidomniim  7445  nninfwlpoimlemg  7479  exmidfodomrlemim  7517  netap  7584  2omotaplemap  7587  xaddcom  10213  xnegdi  10220  xpncan  10223  xleadd1a  10225  xsubge0  10233  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  flqeqceilz  10704  modifeq2int  10772  modfzo0difsn  10781  modsumfzodifsn  10782  iseqf1olemab  10888  iseqf1olemmo  10891  seq3f1olemstep  10900  seqf1oglem1  10905  fser0const  10921  bcval  11136  bccmpl  11141  bcval5  11150  bcpasc  11153  bccl  11154  hashfzp1  11214  hashfibc  11232  ccatsymb  11315  fzowrddc  11364  swrd0g  11377  swrdsbslen  11383  swrdspsleq  11384  pfxclz  11396  pfxccatin12  11450  swrdccat  11452  pfxccat3a  11455  swrdccat3blem  11456  2zsupmax  11936  2zinfmin  11953  xrmaxifle  11956  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxiflemcom  11959  sumdc  12068  sumrbdclem  12088  fsum3cvg  12089  summodclem2a  12092  zsumdc  12095  isumss  12102  fisumss  12103  isumss2  12104  fsumadd  12117  sumsplitdc  12143  fsummulc2  12159  prodrbdclem  12282  fproddccvg  12283  zproddc  12290  prod1dc  12297  prodssdc  12300  fprodssdc  12301  fprodmul  12302  fprodsplitdc  12307  dvdsabseq  12558  bitsmod  12667  gcdval  12680  gcddvds  12684  gcdcl  12687  gcd0id  12700  gcdneg  12703  gcdaddm  12705  dfgcd3  12731  dfgcd2  12735  gcdmultiplez  12742  dvdssq  12752  dvdslcm  12791  lcmcl  12794  lcmneg  12796  lcmgcd  12800  lcmdvds  12801  lcmid  12802  mulgcddvds  12816  cncongr2  12826  prmind2  12842  rpexp  12875  pw2dvdslemn  12887  fermltl  12956  pclemdc  13011  pcxcl  13034  pcgcd  13052  pcmptcl  13065  pcmpt  13066  pcmpt2  13067  pcprod  13069  fldivp1  13071  1arith  13090  unennn  13232  ennnfonelemss  13245  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ctiunctlemudc  13272  bassetsnn  13353  gsumfzz  13750  gsumfzcl  13754  gsumfzreidx  14090  gsumfzsubmcl  14091  gsumfzmptfidmadd  14092  gsumfzmhm  14096  gsumgfsum  14106  gsumfzfsum  14862  znf1o  14925  lgslem4  16002  lgsneg  16023  lgsmod  16025  lgsdilem  16026  lgsdir2  16032  lgsdir  16034  lgsdi  16036  lgsne0  16037  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  lgsquadlem2  16077  lgsquad3  16083  2lgs  16103  umgrclwwlkge2  16523  eupth2lem3lem4fi  16594  eupth2lem3lem7fi  16595  sumdc2  16697  nnsf  16909  nninfsellemsuc  16916  nninffeq  16924  apdifflemr  16957  trimul0or  16971  nconstwlpolem  16977