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  914  pm5.63  915  pm4.83  920  4exmid  930  jaoi2OLD  960  cases  962  cases2  963  exmidneOLD  2659  xpima  5399  ixxun  11455  lgsquadlem2  23094  cusgrasizeindslem2  23851  ifbieq12d2  26372  elimifd  26373  elim2if  26374  elim2ifim  26375  iocinif  26532  hasheuni  26991  voliune  27101  volfiniune  27102  fvresval  28034  cnambfre  28900  tsim1  29401  testable  31995  uunT1  32356  onfrALTVD  32470  ax6e2ndeqVD  32488  ax6e2ndeqALT  32510  bnj1304  32656
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