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 860 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 845
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 846
This theorem is referenced by:  exmidd  894  pm5.62  1017  pm5.63  1018  pm4.83  1023  cases  1041  xpima  6178  fvresval  7351  ssfi  9169  ixxun  13336  trclfvg  14958  mreexexd  17588  lgsquadlem2  26873  numclwwlk3lem2  29626  elimifd  31762  elim2ifim  31764  iocinif  31979  hasheuni  33071  voliune  33215  volfiniune  33216  bnj1304  33818  wl-cases2-dnf  36369  cnambfre  36524  tsim1  36986  rp-isfinite6  42254  or3or  42759  uunT1  43526  onfrALTVD  43637  ax6e2ndeqVD  43655  ax6e2ndeqALT  43677  testable  47800
  Copyright terms: Public domain W3C validator