Theorem exmiddc 831

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 703  DECID wdc 829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-dc 830

This theorem is referenced by:  stdcndcOLD  841  modc  2062  rabxmdc  3446  dcun  3525  ifsbdc  3538  ifcldadc  3555  ifeq1dadc  3556  ifbothdadc  3557  ifbothdc  3558  ifiddc  3559  eqifdc  3560  ifordc  3564  exmid1dc  4186  exmidn0m  4187  exmidundif  4192  exmidundifim  4193  dcextest  4565  dcdifsnid  6483  fidceq  6847  fidifsnen  6848  fimax2gtrilemstep  6878  finexdc  6880  unfiexmid  6895  unsnfidcex  6897  unsnfidcel  6898  undifdcss  6900  ssfirab  6911  fidcenumlemrks  6930  omp1eomlem  7071  difinfsnlem  7076  difinfsn  7077  ctssdc  7090  nnnninf  7102  nnnninfeq2  7105  nninfisol  7109  exmidomniim  7117  nninfwlpoimlemg  7151  exmidfodomrlemim  7178  xaddcom  9818  xnegdi  9825  xpncan  9828  xleadd1a  9830  xsubge0  9838  exfzdc  10196  flqeqceilz  10274  modifeq2int  10342  modfzo0difsn  10351  modsumfzodifsn  10352  iseqf1olemab  10445  iseqf1olemmo  10448  seq3f1olemstep  10457  fser0const  10472  bcval  10683  bccmpl  10688  bcval5  10697  bcpasc  10700  bccl  10701  hashfzp1  10759  2zsupmax  11189  2zinfmin  11206  xrmaxifle  11209  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxiflemcom  11212  sumdc  11321  sumrbdclem  11340  fsum3cvg  11341  summodclem2a  11344  zsumdc  11347  isumss  11354  fisumss  11355  isumss2  11356  fsumadd  11369  sumsplitdc  11395  fsummulc2  11411  prodrbdclem  11534  fproddccvg  11535  zproddc  11542  prod1dc  11549  prodssdc  11552  fprodssdc  11553  fprodmul  11554  fprodsplitdc  11559  dvdsabseq  11807  zsupcllemstep  11900  infssuzex  11904  gcdval  11914  gcddvds  11918  gcdcl  11921  gcd0id  11934  gcdneg  11937  gcdaddm  11939  dfgcd3  11965  dfgcd2  11969  gcdmultiplez  11976  dvdssq  11986  dvdslcm  12023  lcmcl  12026  lcmneg  12028  lcmgcd  12032  lcmdvds  12033  lcmid  12034  mulgcddvds  12048  cncongr2  12058  prmind2  12074  rpexp  12107  pw2dvdslemn  12119  fermltl  12188  pclemdc  12242  pcxcl  12265  pcgcd  12282  pcmptcl  12294  pcmpt  12295  pcmpt2  12296  pcprod  12298  fldivp1  12300  1arith  12319  unennn  12352  ennnfonelemss  12365  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ctiunctlemudc  12392  lgslem4  13698  lgsneg  13719  lgsmod  13721  lgsdilem  13722  lgsdir2  13728  lgsdir  13730  lgsdi  13732  lgsne0  13733  lgsdirnn0  13742  lgsdinn0  13743  sumdc2  13834  nnsf  14038  nninfsellemsuc  14045  nninffeq  14053  apdifflemr  14079  nconstwlpolem  14096