MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exmid Unicode version

Theorem exmid 415
Description: Law of excluded middle, 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. This is an essential distinction of our classical logic and is not a theorem of intuitionistic logic. In intuitionistic logic, if this statement is true for some , then is decideable. (Contributed by NM, 29-Dec-1992.)
Assertion
Ref Expression
exmid

Proof of Theorem exmid
StepHypRef Expression
1 id 22 . 2
21orri 376 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  \/wo 368
This theorem is referenced by:  exmidd  416  pm5.62  923  pm5.63  924  pm4.83  929  4exmid  939  cases  970  exmidneOLD  2663  xpima  5454  ixxun  11574  lgsquadlem2  23630  cusgrasizeindslem2  24474  ifbieq12d2  27420  elimifd  27421  elim2ifim  27423  iocinif  27592  hasheuni  28091  voliune  28201  volfiniune  28202  fvresval  29197  cnambfre  30063  tsim1  30537  testable  33215  uunT1  33577  onfrALTVD  33691  ax6e2ndeqVD  33709  ax6e2ndeqALT  33731  bnj1304  33878  rp-isfinite6  37744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370
  Copyright terms: Public domain W3C validator