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  4339  exmidn0m  4340  exmidundif  4345  exmidundifim  4346  dcextest  4730  dcdifsnid  6781  pw2f1odclem  7138  fidceq  7175  fidifsnen  7176  fidcen  7207  fimax2gtrilemstep  7209  finexdc  7211  elssdc  7213  eqsndc  7214  unfiexmid  7229  unsnfidcex  7231  unsnfidcel  7232  undifdcss  7234  prfidceq  7239  tpfidceq  7241  ssfirab  7248  fidcenumlemrks  7275  2omap  7324  omp1eomlem  7440  difinfsnlem  7445  difinfsn  7446  ctssdc  7459  nnnninf  7472  nnnninfeq2  7475  nninfisol  7479  exmidomniim  7487  nninfwlpoimlemg  7521  exmidfodomrlemim  7559  netap  7626  2omotaplemap  7629  xaddcom  10280  xnegdi  10287  xpncan  10290  xleadd1a  10292  xsubge0  10300  exfzdc  10676  zsupcllemstep  10679  infssuzex  10683  flqeqceilz  10776  modifeq2int  10844  modfzo0difsn  10853  modsumfzodifsn  10854  iseqf1olemab  10960  iseqf1olemmo  10963  seq3f1olemstep  10972  seqf1oglem1  10977  fser0const  10993  bcval  11209  bccmpl  11214  bcval5  11223  bcpasc  11226  bccl  11227  hashfzp1  11287  hashfibc  11305  ccatsymb  11392  fzowrddc  11441  swrd0g  11454  swrdsbslen  11460  swrdspsleq  11461  pfxclz  11473  pfxccatin12  11527  swrdccat  11529  pfxccat3a  11532  swrdccat3blem  11533  2zsupmax  12015  2zinfmin  12034  xrmaxifle  12037  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxiflemcom  12040  sumdc  12149  sumrbdclem  12169  fsum3cvg  12170  summodclem2a  12173  zsumdc  12176  isumss  12183  fisumss  12184  isumss2  12185  fsumadd  12198  sumsplitdc  12224  fsummulc2  12240  prodrbdclem  12363  fproddccvg  12364  zproddc  12371  prod1dc  12378  prodssdc  12381  fprodssdc  12382  fprodmul  12383  fprodsplitdc  12388  dvdsabseq  12639  bitsmod  12748  gcdval  12761  gcddvds  12765  gcdcl  12768  gcd0id  12781  gcdneg  12784  gcdaddm  12786  dfgcd3  12812  dfgcd2  12816  gcdmultiplez  12823  dvdssq  12833  dvdslcm  12872  lcmcl  12875  lcmneg  12877  lcmgcd  12881  lcmdvds  12882  lcmid  12883  mulgcddvds  12897  cncongr2  12907  prmind2  12923  prmdcz  12934  rpexp  12957  pwbdvdslemn  12969  nn0sqdcq  13013  sqrtrirr  13014  fermltl  13041  pclemdc  13096  pcxcl  13119  pcgcd  13137  pcmptcl  13150  pcmpt  13151  pcmpt2  13152  pcprod  13154  fldivp1  13156  1arith  13175  unennn  13346  ennnfonelemss  13359  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ctiunctlemudc  13386  bassetsnn  13467  gzsumcl  13863  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  gzsumgsum  14245  gsumresfi  14263  znf1o  15095  ppiqp1le  16267  chtublem  16295  bposlem1  16311  bposlem3  16313  bposlem5  16315  bposlem6  16316  lgslem4  16327  lgsneg  16348  lgsmod  16350  lgsdilem  16351  lgsdir2  16357  lgsdir  16359  lgsdi  16361  lgsne0  16362  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  lgsquadlem2  16402  lgsquad3  16408  2lgs  16428  umgrclwwlkge2  16848  eupth2lem3lem4fi  16919  eupth2lem3lem7fi  16920  sumdc2  17032  wexmiddifxy  17251  nnsf  17254  nninfsellemsuc  17261  nninffeq  17269  apdifflemr  17303  nconstwlpolem  17322