Theorem exmiddc 843

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 715  DECID wdc 841

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 842

This theorem is referenced by:  stdcndcOLD  853  dfifp2dc  989  ifpiddc  999  modc  2123  rabxmdc  3526  dcun  3604  ifsbdc  3618  ifcldadc  3635  ifeq1dadc  3636  ifeq2dadc  3637  ifeqdadc  3638  ifbothdadc  3639  ifbothdc  3640  ifiddc  3641  eqifdc  3642  2if2dc  3645  ifordc  3647  exmid1dc  4290  exmidn0m  4291  exmidundif  4296  exmidundifim  4297  dcextest  4679  dcdifsnid  6671  pw2f1odclem  7019  fidceq  7055  fidifsnen  7056  fidcen  7087  fimax2gtrilemstep  7089  finexdc  7091  elssdc  7093  eqsndc  7094  unfiexmid  7109  unsnfidcex  7111  unsnfidcel  7112  undifdcss  7114  prfidceq  7119  tpfidceq  7121  ssfirab  7128  fidcenumlemrks  7151  omp1eomlem  7292  difinfsnlem  7297  difinfsn  7298  ctssdc  7311  nnnninf  7324  nnnninfeq2  7327  nninfisol  7331  exmidomniim  7339  nninfwlpoimlemg  7373  exmidfodomrlemim  7411  netap  7472  2omotaplemap  7475  xaddcom  10095  xnegdi  10102  xpncan  10105  xleadd1a  10107  xsubge0  10115  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  flqeqceilz  10579  modifeq2int  10647  modfzo0difsn  10656  modsumfzodifsn  10657  iseqf1olemab  10763  iseqf1olemmo  10766  seq3f1olemstep  10775  seqf1oglem1  10780  fser0const  10796  bcval  11010  bccmpl  11015  bcval5  11024  bcpasc  11027  bccl  11028  hashfzp1  11087  ccatsymb  11178  fzowrddc  11227  swrd0g  11240  swrdsbslen  11246  swrdspsleq  11247  pfxclz  11259  pfxccatin12  11313  swrdccat  11315  pfxccat3a  11318  swrdccat3blem  11319  2zsupmax  11786  2zinfmin  11803  xrmaxifle  11806  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxiflemcom  11809  sumdc  11918  sumrbdclem  11937  fsum3cvg  11938  summodclem2a  11941  zsumdc  11944  isumss  11951  fisumss  11952  isumss2  11953  fsumadd  11966  sumsplitdc  11992  fsummulc2  12008  prodrbdclem  12131  fproddccvg  12132  zproddc  12139  prod1dc  12146  prodssdc  12149  fprodssdc  12150  fprodmul  12151  fprodsplitdc  12156  dvdsabseq  12407  bitsmod  12516  gcdval  12529  gcddvds  12533  gcdcl  12536  gcd0id  12549  gcdneg  12552  gcdaddm  12554  dfgcd3  12580  dfgcd2  12584  gcdmultiplez  12591  dvdssq  12601  dvdslcm  12640  lcmcl  12643  lcmneg  12645  lcmgcd  12649  lcmdvds  12650  lcmid  12651  mulgcddvds  12665  cncongr2  12675  prmind2  12691  rpexp  12724  pw2dvdslemn  12736  fermltl  12805  pclemdc  12860  pcxcl  12883  pcgcd  12901  pcmptcl  12914  pcmpt  12915  pcmpt2  12916  pcprod  12918  fldivp1  12920  1arith  12939  unennn  13017  ennnfonelemss  13030  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ctiunctlemudc  13057  bassetsnn  13138  gsumfzz  13577  gsumfzcl  13581  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  gsumfzfsum  14601  znf1o  14664  lgslem4  15731  lgsneg  15752  lgsmod  15754  lgsdilem  15755  lgsdir2  15761  lgsdir  15763  lgsdi  15765  lgsne0  15766  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  lgsquadlem2  15806  lgsquad3  15812  2lgs  15832  umgrclwwlkge2  16252  sumdc2  16395  2omap  16594  nnsf  16607  nninfsellemsuc  16614  nninffeq  16622  apdifflemr  16651  nconstwlpolem  16669  gsumgfsum  16684