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

Theorem exmid 923
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 893 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 878
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 199  df-or 879
This theorem is referenced by:  exmidd  924  pm5.62  1047  pm5.63  1048  pm4.83  1053  cases  1069  xpima  5817  ixxun  12479  trclfvg  14133  mreexexd  16661  lgsquadlem2  25519  numclwwlk3lem2  27788  elimifd  29899  elim2ifim  29901  iocinif  30079  hasheuni  30681  voliune  30826  volfiniune  30827  bnj1304  31425  fvresval  32196  wl-cases2-dnf  33833  cnambfre  33994  tsim1  34470  rp-isfinite6  38698  or3or  39152  uunT1  39827  onfrALTVD  39938  ax6e2ndeqVD  39956  ax6e2ndeqALT  39978  testable  43435
  Copyright terms: Public domain W3C validator