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 ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 720  DECID wdc 846

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 847

This theorem is referenced by:  stdcndcOLD  858  dfifp2dc  994  ifpiddc  1004  modc  2130  rabxmdc  3554  dcun  3634  ifsbdc  3650  ifcldadc  3667  ifeq1dadc  3668  ifeq2dadc  3669  ifeqdadc  3670  ifbothdadc  3671  ifbothdc  3672  ifiddc  3673  eqifdc  3674  2if2dc  3677  ifordc  3679  ifeqeqxdc  3684  exmid1dc  4332  exmidn0m  4333  exmidundif  4338  exmidundifim  4339  dcextest  4723  dcdifsnid  6767  pw2f1odclem  7124  fidceq  7161  fidifsnen  7162  fidcen  7193  fimax2gtrilemstep  7195  finexdc  7197  elssdc  7199  eqsndc  7200  unfiexmid  7215  unsnfidcex  7217  unsnfidcel  7218  undifdcss  7220  prfidceq  7225  tpfidceq  7227  ssfirab  7234  fidcenumlemrks  7260  2omap  7308  omp1eomlem  7424  difinfsnlem  7429  difinfsn  7430  ctssdc  7443  nnnninf  7456  nnnninfeq2  7459  nninfisol  7463  exmidomniim  7471  nninfwlpoimlemg  7505  exmidfodomrlemim  7543  netap  7610  2omotaplemap  7613  xaddcom  10242  xnegdi  10249  xpncan  10252  xleadd1a  10254  xsubge0  10262  exfzdc  10637  zsupcllemstep  10640  infssuzex  10644  flqeqceilz  10733  modifeq2int  10801  modfzo0difsn  10810  modsumfzodifsn  10811  iseqf1olemab  10917  iseqf1olemmo  10920  seq3f1olemstep  10929  seqf1oglem1  10934  fser0const  10950  bcval  11165  bccmpl  11170  bcval5  11179  bcpasc  11182  bccl  11183  hashfzp1  11243  hashfibc  11261  ccatsymb  11348  fzowrddc  11397  swrd0g  11410  swrdsbslen  11416  swrdspsleq  11417  pfxclz  11429  pfxccatin12  11483  swrdccat  11485  pfxccat3a  11488  swrdccat3blem  11489  2zsupmax  11970  2zinfmin  11987  xrmaxifle  11990  xrmaxiflemab  11991  xrmaxiflemlub  11992  xrmaxiflemcom  11993  sumdc  12102  sumrbdclem  12122  fsum3cvg  12123  summodclem2a  12126  zsumdc  12129  isumss  12136  fisumss  12137  isumss2  12138  fsumadd  12151  sumsplitdc  12177  fsummulc2  12193  prodrbdclem  12316  fproddccvg  12317  zproddc  12324  prod1dc  12331  prodssdc  12334  fprodssdc  12335  fprodmul  12336  fprodsplitdc  12341  dvdsabseq  12592  bitsmod  12701  gcdval  12714  gcddvds  12718  gcdcl  12721  gcd0id  12734  gcdneg  12737  gcdaddm  12739  dfgcd3  12765  dfgcd2  12769  gcdmultiplez  12776  dvdssq  12786  dvdslcm  12825  lcmcl  12828  lcmneg  12830  lcmgcd  12834  lcmdvds  12835  lcmid  12836  mulgcddvds  12850  cncongr2  12860  prmind2  12876  rpexp  12909  pw2dvdslemn  12921  fermltl  12990  pclemdc  13045  pcxcl  13068  pcgcd  13086  pcmptcl  13099  pcmpt  13100  pcmpt2  13101  pcprod  13103  fldivp1  13105  1arith  13124  unennn  13266  ennnfonelemss  13279  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ctiunctlemudc  13306  bassetsnn  13387  gzsumcl  13781  gzsumreidx  14118  gzsumsubmcl  14119  gzsummhm  14122  gzsumgsum  14132  znf1o  14958  lgslem4  16036  lgsneg  16057  lgsmod  16059  lgsdilem  16060  lgsdir2  16066  lgsdir  16068  lgsdi  16070  lgsne0  16071  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  lgsquadlem2  16111  lgsquad3  16117  2lgs  16137  umgrclwwlkge2  16557  eupth2lem3lem4fi  16628  eupth2lem3lem7fi  16629  sumdc2  16741  nnsf  16953  nninfsellemsuc  16960  nninffeq  16968  apdifflemr  17001  nconstwlpolem  17020