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

Theorem exmid 888
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 856 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 841
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 208  df-or 842
This theorem is referenced by:  exmidd  889  pm5.62  1012  pm5.63  1013  pm4.83  1018  cases  1034  xpima  6032  ixxun  12742  trclfvg  14363  mreexexd  16907  lgsquadlem2  25884  numclwwlk3lem2  28090  elimifd  30225  elim2ifim  30227  iocinif  30430  hasheuni  31243  voliune  31387  volfiniune  31388  bnj1304  31990  fvresval  32907  wl-cases2-dnf  34634  cnambfre  34821  tsim1  35289  rp-isfinite6  39762  or3or  40249  uunT1  40991  onfrALTVD  41102  ax6e2ndeqVD  41120  ax6e2ndeqALT  41142  testable  44829
  Copyright terms: Public domain W3C validator