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

Theorem exmiddc 804
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 𝜑 → (𝜑 ∨ ¬ 𝜑))

Proof of Theorem exmiddc
StepHypRef Expression
1 df-dc 803 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
21biimpi 119 1 (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wo 680  DECID wdc 802
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 803
This theorem is referenced by:  stdcndcOLD  814  modc  2018  rabxmdc  3362  dcun  3441  ifsbdc  3454  ifcldadc  3469  ifeq1dadc  3470  ifbothdadc  3471  ifbothdc  3472  ifiddc  3473  eqifdc  3474  exmid1dc  4091  exmidn0m  4092  exmidundif  4097  exmidundifim  4098  dcextest  4463  dcdifsnid  6366  fidceq  6729  fidifsnen  6730  fimax2gtrilemstep  6760  finexdc  6762  unfiexmid  6772  unsnfidcex  6774  unsnfidcel  6775  undifdcss  6777  ssfirab  6788  fidcenumlemrks  6807  omp1eomlem  6945  difinfsnlem  6950  difinfsn  6951  ctssdc  6964  exmidomniim  6979  nnnninf  6989  exmidfodomrlemim  7021  xaddcom  9584  xnegdi  9591  xpncan  9594  xleadd1a  9596  xsubge0  9604  exfzdc  9957  flqeqceilz  10031  modifeq2int  10099  modfzo0difsn  10108  modsumfzodifsn  10109  iseqf1olemab  10202  iseqf1olemmo  10205  seq3f1olemstep  10214  fser0const  10229  bcval  10435  bccmpl  10440  bcval5  10449  bcpasc  10452  bccl  10453  hashfzp1  10510  2zsupmax  10937  xrmaxifle  10955  xrmaxiflemab  10956  xrmaxiflemlub  10957  xrmaxiflemcom  10958  sumdc  11067  sumrbdclem  11085  fsum3cvg  11086  summodclem2a  11090  zsumdc  11093  isumss  11100  fisumss  11101  isumss2  11102  fsumadd  11115  sumsplitdc  11141  fsummulc2  11157  dvdsabseq  11441  zsupcllemstep  11534  infssuzex  11538  gcdval  11544  gcddvds  11548  gcdcl  11551  gcd0id  11563  gcdneg  11566  gcdaddm  11568  dfgcd3  11594  dfgcd2  11598  gcdmultiplez  11605  dvdssq  11615  dvdslcm  11646  lcmcl  11649  lcmneg  11651  lcmgcd  11655  lcmdvds  11656  lcmid  11657  mulgcddvds  11671  cncongr2  11681  prmind2  11697  rpexp  11727  pw2dvdslemn  11738  unennn  11805  ennnfonelemss  11818  ennnfonelemkh  11820  ennnfonelemhf1o  11821  ctiunctlemudc  11845  sumdc2  12829  nnsf  13022  nninfsellemsuc  13031  nninffeq  13039
  Copyright terms: Public domain W3C validator