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  10769  modifeq2int  10837  modfzo0difsn  10846  modsumfzodifsn  10847  iseqf1olemab  10953  iseqf1olemmo  10956  seq3f1olemstep  10965  seqf1oglem1  10970  fser0const  10986  bcval  11202  bccmpl  11207  bcval5  11216  bcpasc  11219  bccl  11220  hashfzp1  11280  hashfibc  11298  ccatsymb  11385  fzowrddc  11434  swrd0g  11447  swrdsbslen  11453  swrdspsleq  11454  pfxclz  11466  pfxccatin12  11520  swrdccat  11522  pfxccat3a  11525  swrdccat3blem  11526  2zsupmax  12008  2zinfmin  12027  xrmaxifle  12030  xrmaxiflemab  12031  xrmaxiflemlub  12032  xrmaxiflemcom  12033  sumdc  12142  sumrbdclem  12162  fsum3cvg  12163  summodclem2a  12166  zsumdc  12169  isumss  12176  fisumss  12177  isumss2  12178  fsumadd  12191  sumsplitdc  12217  fsummulc2  12233  prodrbdclem  12356  fproddccvg  12357  zproddc  12364  prod1dc  12371  prodssdc  12374  fprodssdc  12375  fprodmul  12376  fprodsplitdc  12381  dvdsabseq  12632  bitsmod  12741  gcdval  12754  gcddvds  12758  gcdcl  12761  gcd0id  12774  gcdneg  12777  gcdaddm  12779  dfgcd3  12805  dfgcd2  12809  gcdmultiplez  12816  dvdssq  12826  dvdslcm  12865  lcmcl  12868  lcmneg  12870  lcmgcd  12874  lcmdvds  12875  lcmid  12876  mulgcddvds  12890  cncongr2  12900  prmind2  12916  prmdcz  12927  rpexp  12950  pwbdvdslemn  12962  nn0sqdcq  13006  sqrtrirr  13007  fermltl  13034  pclemdc  13089  pcxcl  13112  pcgcd  13130  pcmptcl  13143  pcmpt  13144  pcmpt2  13145  pcprod  13147  fldivp1  13149  1arith  13168  unennn  13339  ennnfonelemss  13352  ennnfonelemkh  13354  ennnfonelemhf1o  13355  ctiunctlemudc  13379  bassetsnn  13460  gzsumcl  13855  gzsumreidx  14192  gzsumsubmcl  14193  gzsummhm  14196  gzsumgsum  14206  znf1o  15037  ppiqp1le  16189  chtublem  16217  bposlem1  16233  bposlem3  16235  bposlem5  16237  lgslem4  16244  lgsneg  16265  lgsmod  16267  lgsdilem  16268  lgsdir2  16274  lgsdir  16276  lgsdi  16278  lgsne0  16279  lgsdirnn0  16288  lgsdinn0  16289  gausslemma2dlem1a  16299  gausslemma2dlem1f1o  16301  lgsquadlem2  16319  lgsquad3  16325  2lgs  16345  umgrclwwlkge2  16765  eupth2lem3lem4fi  16836  eupth2lem3lem7fi  16837  sumdc2  16949  wexmiddifxy  17168  nnsf  17170  nninfsellemsuc  17177  nninffeq  17185  apdifflemr  17218  nconstwlpolem  17237