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

Theorem exmid 893
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 decidable. (Contributed by NM, 29-Dec-1992.)
Assertion
Ref Expression
exmid (𝜑 ∨ ¬ 𝜑)

Proof of Theorem exmid
StepHypRef Expression
1 id 22 . 2 𝜑 → ¬ 𝜑)
21orri 861 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 846
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 206  df-or 847
This theorem is referenced by:  exmidd  894  pm5.62  1017  pm5.63  1018  pm4.83  1023  cases  1041  xpima  6180  fvresval  7360  ssfi  9189  ixxun  13364  trclfvg  14986  mreexexd  17619  lgsquadlem2  27301  numclwwlk3lem2  30181  elimifd  32319  elim2ifim  32321  iocinif  32533  hasheuni  33640  voliune  33784  volfiniune  33785  bnj1304  34386  wl-cases2-dnf  36915  cnambfre  37076  tsim1  37538  rp-isfinite6  42871  or3or  43376  uunT1  44142  onfrALTVD  44253  ax6e2ndeqVD  44271  ax6e2ndeqALT  44293  testable  48156
  Copyright terms: Public domain W3C validator