ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exmiddc Unicode version

Theorem exmiddc 836
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
StepHypRef Expression
1 df-dc 835 . 2  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
21biimpi 120 1  |-  (DECID  ph  ->  (
ph  \/  -.  ph )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 708  DECID wdc 834
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 835
This theorem is referenced by:  stdcndcOLD  846  modc  2069  rabxmdc  3454  dcun  3533  ifsbdc  3546  ifcldadc  3563  ifeq1dadc  3564  ifbothdadc  3565  ifbothdc  3566  ifiddc  3567  eqifdc  3568  ifordc  3572  exmid1dc  4197  exmidn0m  4198  exmidundif  4203  exmidundifim  4204  dcextest  4576  dcdifsnid  6498  fidceq  6862  fidifsnen  6863  fimax2gtrilemstep  6893  finexdc  6895  unfiexmid  6910  unsnfidcex  6912  unsnfidcel  6913  undifdcss  6915  ssfirab  6926  fidcenumlemrks  6945  omp1eomlem  7086  difinfsnlem  7091  difinfsn  7092  ctssdc  7105  nnnninf  7117  nnnninfeq2  7120  nninfisol  7124  exmidomniim  7132  nninfwlpoimlemg  7166  exmidfodomrlemim  7193  xaddcom  9835  xnegdi  9842  xpncan  9845  xleadd1a  9847  xsubge0  9855  exfzdc  10213  flqeqceilz  10291  modifeq2int  10359  modfzo0difsn  10368  modsumfzodifsn  10369  iseqf1olemab  10462  iseqf1olemmo  10465  seq3f1olemstep  10474  fser0const  10489  bcval  10700  bccmpl  10705  bcval5  10714  bcpasc  10717  bccl  10718  hashfzp1  10775  2zsupmax  11205  2zinfmin  11222  xrmaxifle  11225  xrmaxiflemab  11226  xrmaxiflemlub  11227  xrmaxiflemcom  11228  sumdc  11337  sumrbdclem  11356  fsum3cvg  11357  summodclem2a  11360  zsumdc  11363  isumss  11370  fisumss  11371  isumss2  11372  fsumadd  11385  sumsplitdc  11411  fsummulc2  11427  prodrbdclem  11550  fproddccvg  11551  zproddc  11558  prod1dc  11565  prodssdc  11568  fprodssdc  11569  fprodmul  11570  fprodsplitdc  11575  dvdsabseq  11823  zsupcllemstep  11916  infssuzex  11920  gcdval  11930  gcddvds  11934  gcdcl  11937  gcd0id  11950  gcdneg  11953  gcdaddm  11955  dfgcd3  11981  dfgcd2  11985  gcdmultiplez  11992  dvdssq  12002  dvdslcm  12039  lcmcl  12042  lcmneg  12044  lcmgcd  12048  lcmdvds  12049  lcmid  12050  mulgcddvds  12064  cncongr2  12074  prmind2  12090  rpexp  12123  pw2dvdslemn  12135  fermltl  12204  pclemdc  12258  pcxcl  12281  pcgcd  12298  pcmptcl  12310  pcmpt  12311  pcmpt2  12312  pcprod  12314  fldivp1  12316  1arith  12335  unennn  12368  ennnfonelemss  12381  ennnfonelemkh  12383  ennnfonelemhf1o  12384  ctiunctlemudc  12408  lgslem4  14037  lgsneg  14058  lgsmod  14060  lgsdilem  14061  lgsdir2  14067  lgsdir  14069  lgsdi  14071  lgsne0  14072  lgsdirnn0  14081  lgsdinn0  14082  sumdc2  14173  nnsf  14377  nninfsellemsuc  14384  nninffeq  14392  apdifflemr  14418  nconstwlpolem  14435
  Copyright terms: Public domain W3C validator