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

Theorem exmid 430
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 390 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 382
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 384
This theorem is referenced by:  exmidd  431  pm5.62  996  pm5.63  997  pm4.83  1008  cases  1029  4exmidOLD  1040  xpima  5726  ixxun  12376  trclfvg  13947  mreexexd  16502  lgsquadlem2  25297  numclwwlk3lem  27544  elimifd  29661  elim2ifim  29663  iocinif  29844  hasheuni  30448  voliune  30593  volfiniune  30594  bnj1304  31189  fvresval  31964  wl-cases2-dnf  33600  cnambfre  33763  tsim1  34242  rp-isfinite6  38358  or3or  38813  uunT1  39501  onfrALTVD  39618  ax6e2ndeqVD  39636  ax6e2ndeqALT  39658  testable  43051
  Copyright terms: Public domain W3C validator