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

Proof of Theorem exmiddc

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

This proof depends on syntax axioms:   -. wn 3   -> wi 4   \/ wo 720  DECID wdc 846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

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

This theorem is used 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  4337  exmidn0m  4338  exmidundif  4343  exmidundifim  4344  dcextest  4728  dcdifsnid  6777  pw2f1odclem  7134  fidceq  7171  fidifsnen  7172  fidcen  7203  fimax2gtrilemstep  7205  finexdc  7207  elssdc  7209  eqsndc  7210  unfiexmid  7225  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  prfidceq  7235  tpfidceq  7237  ssfirab  7244  fidcenumlemrks  7270  2omap  7319  omp1eomlem  7435  difinfsnlem  7440  difinfsn  7441  ctssdc  7454  nnnninf  7467  nnnninfeq2  7470  nninfisol  7474  exmidomniim  7482  nninfwlpoimlemg  7516  exmidfodomrlemim  7554  netap  7621  2omotaplemap  7624  xaddcom  10274  xnegdi  10281  xpncan  10284  xleadd1a  10286  xsubge0  10294  exfzdc  10670  zsupcllemstep  10673  infssuzex  10677  flqeqceilz  10770  modifeq2int  10838  modfzo0difsn  10847  modsumfzodifsn  10848  iseqf1olemab  10954  iseqf1olemmo  10957  seq3f1olemstep  10966  seqf1oglem1  10971  fser0const  10987  bcval  11203  bccmpl  11208  bcval5  11217  bcpasc  11220  bccl  11221  hashfzp1  11281  hashfibc  11299  ccatsymb  11386  fzowrddc  11435  swrd0g  11448  swrdsbslen  11454  swrdspsleq  11455  pfxclz  11467  pfxccatin12  11521  swrdccat  11523  pfxccat3a  11526  swrdccat3blem  11527  2zsupmax  12009  2zinfmin  12028  xrmaxifle  12031  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxiflemcom  12034  sumdc  12143  sumrbdclem  12163  fsum3cvg  12164  summodclem2a  12167  zsumdc  12170  isumss  12177  fisumss  12178  isumss2  12179  fsumadd  12192  sumsplitdc  12218  fsummulc2  12234  prodrbdclem  12357  fproddccvg  12358  zproddc  12365  prod1dc  12372  prodssdc  12375  fprodssdc  12376  fprodmul  12377  fprodsplitdc  12382  dvdsabseq  12633  bitsmod  12742  gcdval  12755  gcddvds  12759  gcdcl  12762  gcd0id  12775  gcdneg  12778  gcdaddm  12780  dfgcd3  12806  dfgcd2  12810  gcdmultiplez  12817  dvdssq  12827  dvdslcm  12866  lcmcl  12869  lcmneg  12871  lcmgcd  12875  lcmdvds  12876  lcmid  12877  mulgcddvds  12891  cncongr2  12901  prmind2  12917  prmdcz  12928  rpexp  12951  pwbdvdslemn  12963  nn0sqdcq  13007  sqrtrirr  13008  fermltl  13035  pclemdc  13090  pcxcl  13113  pcgcd  13131  pcmptcl  13144  pcmpt  13145  pcmpt2  13146  pcprod  13148  fldivp1  13150  1arith  13169  unennn  13340  ennnfonelemss  13353  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ctiunctlemudc  13380  bassetsnn  13461  gzsumcl  13857  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  gzsumgsum  14239  znf1o  15070  ppiqp1le  16228  chtublem  16256  bposlem1  16272  bposlem3  16274  bposlem5  16276  bposlem6  16277  lgslem4  16288  lgsneg  16309  lgsmod  16311  lgsdilem  16312  lgsdir2  16318  lgsdir  16320  lgsdi  16322  lgsne0  16323  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  lgsquadlem2  16363  lgsquad3  16369  2lgs  16389  umgrclwwlkge2  16809  eupth2lem3lem4fi  16880  eupth2lem3lem7fi  16881  sumdc2  16993  wexmiddifxy  17212  nnsf  17214  nninfsellemsuc  17221  nninffeq  17229  apdifflemr  17263  nconstwlpolem  17282