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

Theorem exmid 891
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 858 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 843
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 209  df-or 844
This theorem is referenced by:  exmidd  892  pm5.62  1015  pm5.63  1016  pm4.83  1021  cases  1037  xpima  6032  ixxun  12746  trclfvg  14367  mreexexd  16911  lgsquadlem2  25949  numclwwlk3lem2  28155  elimifd  30290  elim2ifim  30292  iocinif  30496  hasheuni  31337  voliune  31481  volfiniune  31482  bnj1304  32084  fvresval  33003  wl-cases2-dnf  34744  cnambfre  34932  tsim1  35400  rp-isfinite6  39875  or3or  40362  uunT1  41105  onfrALTVD  41216  ax6e2ndeqVD  41234  ax6e2ndeqALT  41256  testable  44892
  Copyright terms: Public domain W3C validator