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

Theorem exmid 894
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 862 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 847
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 848
This theorem is referenced by:  exmidd  895  pm5.62  1020  pm5.63  1021  pm4.83  1026  cases  1042  xpima  6204  fvresval  7378  ssfi  9212  ixxun  13400  trclfvg  15051  mreexexd  17693  lgsquadlem2  27440  numclwwlk3lem2  30413  elimifd  32564  elim2ifim  32566  iocinif  32790  hasheuni  34066  voliune  34210  volfiniune  34211  bnj1304  34812  wl-cases2-dnf  37493  cnambfre  37655  tsim1  38117  rp-isfinite6  43508  or3or  44013  uunT1  44778  onfrALTVD  44889  ax6e2ndeqVD  44907  ax6e2ndeqALT  44929  testable  49031
  Copyright terms: Public domain W3C validator