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

Theorem exmid 429
 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 389 1 (𝜑 ∨ ¬ 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∨ wo 381 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 195  df-or 383 This theorem is referenced by:  exmidd  430  pm5.62  959  pm5.63  960  pm4.83  965  4exmid  976  cases  1003  xpima  5385  ixxun  11930  trclfvg  13461  mreexexd  16021  lgsquadlem2  24796  cusgrasizeindslem1  25741  elimifd  28535  elim2ifim  28537  iocinif  28729  hasheuni  29271  voliune  29416  volfiniune  29417  bnj1304  29990  fvresval  30754  wl-cases2-dnf  32348  cnambfre  32503  tsim1  32982  rp-isfinite6  36765  or3or  37221  uunT1  37910  onfrALTVD  38031  ax6e2ndeqVD  38049  ax6e2ndeqALT  38071  testable  42408
 Copyright terms: Public domain W3C validator