Theorem exmiddc 841

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 713  DECID wdc 839

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 840

This theorem is referenced by:  stdcndcOLD  851  dfifp2dc  987  ifpiddc  997  modc  2121  rabxmdc  3523  dcun  3601  ifsbdc  3615  ifcldadc  3632  ifeq1dadc  3633  ifeq2dadc  3634  ifeqdadc  3635  ifbothdadc  3636  ifbothdc  3637  ifiddc  3638  eqifdc  3639  2if2dc  3642  ifordc  3644  exmid1dc  4283  exmidn0m  4284  exmidundif  4289  exmidundifim  4290  dcextest  4672  dcdifsnid  6648  pw2f1odclem  6991  fidceq  7027  fidifsnen  7028  fimax2gtrilemstep  7058  finexdc  7060  unfiexmid  7076  unsnfidcex  7078  unsnfidcel  7079  undifdcss  7081  prfidceq  7086  tpfidceq  7088  ssfirab  7094  fidcenumlemrks  7116  omp1eomlem  7257  difinfsnlem  7262  difinfsn  7263  ctssdc  7276  nnnninf  7289  nnnninfeq2  7292  nninfisol  7296  exmidomniim  7304  nninfwlpoimlemg  7338  exmidfodomrlemim  7375  netap  7436  2omotaplemap  7439  xaddcom  10053  xnegdi  10060  xpncan  10063  xleadd1a  10065  xsubge0  10073  exfzdc  10441  zsupcllemstep  10444  infssuzex  10448  flqeqceilz  10535  modifeq2int  10603  modfzo0difsn  10612  modsumfzodifsn  10613  iseqf1olemab  10719  iseqf1olemmo  10722  seq3f1olemstep  10731  seqf1oglem1  10736  fser0const  10752  bcval  10966  bccmpl  10971  bcval5  10980  bcpasc  10983  bccl  10984  hashfzp1  11041  ccatsymb  11132  fzowrddc  11174  swrd0g  11187  swrdsbslen  11193  swrdspsleq  11194  pfxclz  11206  pfxccatin12  11260  swrdccat  11262  pfxccat3a  11265  swrdccat3blem  11266  2zsupmax  11732  2zinfmin  11749  xrmaxifle  11752  xrmaxiflemab  11753  xrmaxiflemlub  11754  xrmaxiflemcom  11755  sumdc  11864  sumrbdclem  11883  fsum3cvg  11884  summodclem2a  11887  zsumdc  11890  isumss  11897  fisumss  11898  isumss2  11899  fsumadd  11912  sumsplitdc  11938  fsummulc2  11954  prodrbdclem  12077  fproddccvg  12078  zproddc  12085  prod1dc  12092  prodssdc  12095  fprodssdc  12096  fprodmul  12097  fprodsplitdc  12102  dvdsabseq  12353  bitsmod  12462  gcdval  12475  gcddvds  12479  gcdcl  12482  gcd0id  12495  gcdneg  12498  gcdaddm  12500  dfgcd3  12526  dfgcd2  12530  gcdmultiplez  12537  dvdssq  12547  dvdslcm  12586  lcmcl  12589  lcmneg  12591  lcmgcd  12595  lcmdvds  12596  lcmid  12597  mulgcddvds  12611  cncongr2  12621  prmind2  12637  rpexp  12670  pw2dvdslemn  12682  fermltl  12751  pclemdc  12806  pcxcl  12829  pcgcd  12847  pcmptcl  12860  pcmpt  12861  pcmpt2  12862  pcprod  12864  fldivp1  12866  1arith  12885  unennn  12963  ennnfonelemss  12976  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ctiunctlemudc  13003  bassetsnn  13084  gsumfzz  13523  gsumfzcl  13527  gsumfzreidx  13869  gsumfzsubmcl  13870  gsumfzmptfidmadd  13871  gsumfzmhm  13875  gsumfzfsum  14546  znf1o  14609  lgslem4  15676  lgsneg  15697  lgsmod  15699  lgsdilem  15700  lgsdir2  15706  lgsdir  15708  lgsdi  15710  lgsne0  15711  lgsdirnn0  15720  lgsdinn0  15721  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  lgsquadlem2  15751  lgsquad3  15757  2lgs  15777  sumdc2  16121  2omap  16318  nnsf  16330  nninfsellemsuc  16337  nninffeq  16345  apdifflemr  16374  nconstwlpolem  16392