Theorem exmiddc 821

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

Syntax hints:   -. wn 3   -> wi 4   \/ wo 697  DECID wdc 819

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 820

This theorem is referenced by:  stdcndcOLD  831  modc  2042  rabxmdc  3394  dcun  3473  ifsbdc  3486  ifcldadc  3501  ifeq1dadc  3502  ifbothdadc  3503  ifbothdc  3504  ifiddc  3505  eqifdc  3506  exmid1dc  4123  exmidn0m  4124  exmidundif  4129  exmidundifim  4130  dcextest  4495  dcdifsnid  6400  fidceq  6763  fidifsnen  6764  fimax2gtrilemstep  6794  finexdc  6796  unfiexmid  6806  unsnfidcex  6808  unsnfidcel  6809  undifdcss  6811  ssfirab  6822  fidcenumlemrks  6841  omp1eomlem  6979  difinfsnlem  6984  difinfsn  6985  ctssdc  6998  exmidomniim  7013  nnnninf  7023  exmidfodomrlemim  7057  xaddcom  9644  xnegdi  9651  xpncan  9654  xleadd1a  9656  xsubge0  9664  exfzdc  10017  flqeqceilz  10091  modifeq2int  10159  modfzo0difsn  10168  modsumfzodifsn  10169  iseqf1olemab  10262  iseqf1olemmo  10265  seq3f1olemstep  10274  fser0const  10289  bcval  10495  bccmpl  10500  bcval5  10509  bcpasc  10512  bccl  10513  hashfzp1  10570  2zsupmax  10997  xrmaxifle  11015  xrmaxiflemab  11016  xrmaxiflemlub  11017  xrmaxiflemcom  11018  sumdc  11127  sumrbdclem  11146  fsum3cvg  11147  summodclem2a  11150  zsumdc  11153  isumss  11160  fisumss  11161  isumss2  11162  fsumadd  11175  sumsplitdc  11201  fsummulc2  11217  prodrbdclem  11340  fproddccvg  11341  dvdsabseq  11545  zsupcllemstep  11638  infssuzex  11642  gcdval  11648  gcddvds  11652  gcdcl  11655  gcd0id  11667  gcdneg  11670  gcdaddm  11672  dfgcd3  11698  dfgcd2  11702  gcdmultiplez  11709  dvdssq  11719  dvdslcm  11750  lcmcl  11753  lcmneg  11755  lcmgcd  11759  lcmdvds  11760  lcmid  11761  mulgcddvds  11775  cncongr2  11785  prmind2  11801  rpexp  11831  pw2dvdslemn  11843  unennn  11910  ennnfonelemss  11923  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ctiunctlemudc  11950  sumdc2  13006  nnsf  13199  nninfsellemsuc  13208  nninffeq  13216