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

Theorem exmid 880
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 851 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 836
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 197  df-or 837
This theorem is referenced by:  exmidd  881  pm5.62  1004  pm5.63  1005  pm4.83  1010  cases  1027  4exmidOLD  1038  xpima  5717  ixxun  12396  trclfvg  13964  mreexexd  16516  lgsquadlem2  25327  numclwwlk3lem2  27583  elimifd  29700  elim2ifim  29702  iocinif  29883  hasheuni  30487  voliune  30632  volfiniune  30633  bnj1304  31228  fvresval  32003  wl-cases2-dnf  33632  cnambfre  33790  tsim1  34269  rp-isfinite6  38390  or3or  38845  uunT1  39532  onfrALTVD  39649  ax6e2ndeqVD  39667  ax6e2ndeqALT  39689  testable  43077
  Copyright terms: Public domain W3C validator