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

Theorem exmid 895
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 863 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 848
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 207  df-or 849
This theorem is referenced by:  exmidd  896  pm5.62  1021  pm5.63  1022  pm4.83  1027  cases  1043  xpima  6202  fvresval  7378  ssfi  9213  ixxun  13403  trclfvg  15054  mreexexd  17691  lgsquadlem2  27425  numclwwlk3lem2  30403  elimifd  32556  elim2ifim  32558  iocinif  32783  hasheuni  34086  voliune  34230  volfiniune  34231  bnj1304  34833  wl-cases2-dnf  37513  cnambfre  37675  tsim1  38137  rp-isfinite6  43531  or3or  44036  uunT1  44800  onfrALTVD  44911  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  testable  49319
  Copyright terms: Public domain W3C validator