Theorem exmiddc 838

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 837	. 2 |- (DECID ph <-> ( ph \/ -. ph ) )
2	1	biimpi 120	1 |- (DECID ph -> ( ph \/ -. ph ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 710  DECID wdc 836

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 837

This theorem is referenced by:  stdcndcOLD  848  modc  2099  rabxmdc  3500  dcun  3578  ifsbdc  3592  ifcldadc  3609  ifeq1dadc  3610  ifeq2dadc  3611  ifeqdadc  3612  ifbothdadc  3613  ifbothdc  3614  ifiddc  3615  eqifdc  3616  2if2dc  3619  ifordc  3621  exmid1dc  4260  exmidn0m  4261  exmidundif  4266  exmidundifim  4267  dcextest  4647  dcdifsnid  6613  pw2f1odclem  6956  fidceq  6992  fidifsnen  6993  fimax2gtrilemstep  7023  finexdc  7025  unfiexmid  7041  unsnfidcex  7043  unsnfidcel  7044  undifdcss  7046  prfidceq  7051  tpfidceq  7053  ssfirab  7059  fidcenumlemrks  7081  omp1eomlem  7222  difinfsnlem  7227  difinfsn  7228  ctssdc  7241  nnnninf  7254  nnnninfeq2  7257  nninfisol  7261  exmidomniim  7269  nninfwlpoimlemg  7303  exmidfodomrlemim  7340  netap  7401  2omotaplemap  7404  xaddcom  10018  xnegdi  10025  xpncan  10028  xleadd1a  10030  xsubge0  10038  exfzdc  10406  zsupcllemstep  10409  infssuzex  10413  flqeqceilz  10500  modifeq2int  10568  modfzo0difsn  10577  modsumfzodifsn  10578  iseqf1olemab  10684  iseqf1olemmo  10687  seq3f1olemstep  10696  seqf1oglem1  10701  fser0const  10717  bcval  10931  bccmpl  10936  bcval5  10945  bcpasc  10948  bccl  10949  hashfzp1  11006  ccatsymb  11096  fzowrddc  11138  swrd0g  11151  swrdsbslen  11157  swrdspsleq  11158  pfxclz  11170  pfxccatin12  11224  swrdccat  11226  pfxccat3a  11229  swrdccat3blem  11230  2zsupmax  11652  2zinfmin  11669  xrmaxifle  11672  xrmaxiflemab  11673  xrmaxiflemlub  11674  xrmaxiflemcom  11675  sumdc  11784  sumrbdclem  11803  fsum3cvg  11804  summodclem2a  11807  zsumdc  11810  isumss  11817  fisumss  11818  isumss2  11819  fsumadd  11832  sumsplitdc  11858  fsummulc2  11874  prodrbdclem  11997  fproddccvg  11998  zproddc  12005  prod1dc  12012  prodssdc  12015  fprodssdc  12016  fprodmul  12017  fprodsplitdc  12022  dvdsabseq  12273  bitsmod  12382  gcdval  12395  gcddvds  12399  gcdcl  12402  gcd0id  12415  gcdneg  12418  gcdaddm  12420  dfgcd3  12446  dfgcd2  12450  gcdmultiplez  12457  dvdssq  12467  dvdslcm  12506  lcmcl  12509  lcmneg  12511  lcmgcd  12515  lcmdvds  12516  lcmid  12517  mulgcddvds  12531  cncongr2  12541  prmind2  12557  rpexp  12590  pw2dvdslemn  12602  fermltl  12671  pclemdc  12726  pcxcl  12749  pcgcd  12767  pcmptcl  12780  pcmpt  12781  pcmpt2  12782  pcprod  12784  fldivp1  12786  1arith  12805  unennn  12883  ennnfonelemss  12896  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ctiunctlemudc  12923  gsumfzz  13442  gsumfzcl  13446  gsumfzreidx  13788  gsumfzsubmcl  13789  gsumfzmptfidmadd  13790  gsumfzmhm  13794  gsumfzfsum  14465  znf1o  14528  lgslem4  15595  lgsneg  15616  lgsmod  15618  lgsdilem  15619  lgsdir2  15625  lgsdir  15627  lgsdi  15629  lgsne0  15630  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem1a  15650  gausslemma2dlem1f1o  15652  lgsquadlem2  15670  lgsquad3  15676  2lgs  15696  sumdc2  15935  2omap  16132  nnsf  16144  nninfsellemsuc  16151  nninffeq  16159  apdifflemr  16188  nconstwlpolem  16206