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  4339  exmidn0m  4340  exmidundif  4345  exmidundifim  4346  dcextest  4730  dcdifsnid  6782  pw2f1odclem  7140  fidceq  7177  fidifsnen  7178  fidcen  7209  fimax2gtrilemstep  7211  finexdc  7213  elssdc  7215  eqsndc  7216  unfiexmid  7231  unsnfidcex  7233  unsnfidcel  7234  undifdcss  7236  prfidceq  7241  tpfidceq  7243  ssfirab  7250  fidcenumlemrks  7277  2omap  7324  omp1eomlem  7440  difinfsnlem  7445  difinfsn  7446  ctssdc  7459  nnnninf  7472  nnnninfeq2  7475  nninfisol  7479  exmidomniim  7487  nninfwlpoimlemg  7521  exmidfodomrlemim  7559  netap  7626  2omotaplemap  7629  xaddcom  10279  xnegdi  10286  xpncan  10289  xleadd1a  10291  xsubge0  10299  exfzdc  10675  zsupcllemstep  10678  infssuzex  10682  flqeqceilz  10775  modifeq2int  10843  modfzo0difsn  10852  modsumfzodifsn  10853  iseqf1olemab  10959  iseqf1olemmo  10962  seq3f1olemstep  10971  seqf1oglem1  10976  fser0const  10992  bcval  11208  bccmpl  11213  bcval5  11222  bcpasc  11225  bccl  11226  hashfzp1  11286  hashfibc  11304  ccatsymb  11391  fzowrddc  11440  swrd0g  11453  swrdsbslen  11459  swrdspsleq  11460  pfxclz  11472  pfxccatin12  11526  swrdccat  11528  pfxccat3a  11531  swrdccat3blem  11532  2zsupmax  12014  2zinfmin  12033  xrmaxifle  12036  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxiflemcom  12039  sumdc  12148  sumrbdclem  12168  fsum3cvg  12169  summodclem2a  12172  zsumdc  12175  isumss  12182  fisumss  12183  isumss2  12184  fsumadd  12197  sumsplitdc  12223  fsummulc2  12239  prodrbdclem  12362  fproddccvg  12363  zproddc  12370  prod1dc  12377  prodssdc  12380  fprodssdc  12381  fprodmul  12382  fprodsplitdc  12387  dvdsabseq  12638  bitsmod  12747  gcdval  12760  gcddvds  12764  gcdcl  12767  gcd0id  12780  gcdneg  12783  gcdaddm  12785  dfgcd3  12811  dfgcd2  12815  gcdmultiplez  12822  dvdssq  12832  dvdslcm  12871  lcmcl  12874  lcmneg  12876  lcmgcd  12880  lcmdvds  12881  lcmid  12882  mulgcddvds  12896  cncongr2  12906  prmind2  12922  prmdcz  12933  rpexp  12956  pwbdvdslemn  12968  nn0sqdcq  13012  sqrtrirr  13013  fermltl  13040  pclemdc  13095  pcxcl  13118  pcgcd  13136  pcmptcl  13149  pcmpt  13150  pcmpt2  13151  pcprod  13153  fldivp1  13155  1arith  13174  unennn  13345  ennnfonelemss  13358  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ctiunctlemudc  13385  bassetsnn  13466  gzsumcl  13862  gzsumreidx  14230  gzsumsubmcl  14231  gzsummhm  14234  gzsumgsum  14244  gsumresfi  14262  znf1o  15094  ppiqp1le  16284  chtublem  16312  bposlem1  16328  bposlem3  16330  bposlem5  16332  bposlem6  16333  lgslem4  16344  lgsneg  16365  lgsmod  16367  lgsdilem  16368  lgsdir2  16374  lgsdir  16376  lgsdi  16378  lgsne0  16379  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  lgsquadlem2  16419  lgsquad3  16425  2lgs  16445  umgrclwwlkge2  16865  eupth2lem3lem4fi  16936  eupth2lem3lem7fi  16937  sumdc2  17049  wexmiddifxy  17268  nnsf  17271  nninfsellemsuc  17278  nninffeq  17286  apdifflemr  17320  nconstwlpolem  17339