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

Theorem exmid 892
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 859 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 844
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 845
This theorem is referenced by:  exmidd  893  pm5.62  1016  pm5.63  1017  pm4.83  1022  cases  1040  xpima  6085  ssfi  8956  ixxun  13095  trclfvg  14726  mreexexd  17357  lgsquadlem2  26529  numclwwlk3lem2  28748  elimifd  30886  elim2ifim  30888  iocinif  31102  hasheuni  32053  voliune  32197  volfiniune  32198  bnj1304  32799  fvresval  33741  wl-cases2-dnf  35671  cnambfre  35825  tsim1  36288  rp-isfinite6  41125  or3or  41631  uunT1  42400  onfrALTVD  42511  ax6e2ndeqVD  42529  ax6e2ndeqALT  42551  testable  46504
  Copyright terms: Public domain W3C validator