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

Theorem exmid 424
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 385 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 377
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 192  df-or 379
This theorem is referenced by:  exmidd  425  pm5.62  950  pm5.63  951  pm4.83  956  4exmid  967  cases  994  xpima  5329  ixxun  11746  trclfvg  13239  mreexexd  15719  lgsquadlem2  24444  cusgrasizeindslem2  25363  ifbieq12d2  28319  elimifd  28320  elim2ifim  28322  iocinif  28519  hasheuni  29061  voliune  29206  volfiniune  29207  bnj1304  29783  fvresval  30559  wl-cases2-dnf  32071  cnambfre  32227  tsim1  32608  rp-isfinite6  36403  uunT1  37515  onfrALTVD  37636  ax6e2ndeqVD  37654  ax6e2ndeqALT  37676  testable  41726
  Copyright terms: Public domain W3C validator