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

Theorem exmid 431
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 391 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 383
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 385
This theorem is referenced by:  exmidd  432  pm5.62  957  pm5.63  958  pm4.83  969  cases  991  4exmidOLD  997  xpima  5545  ixxun  12149  trclfvg  13706  mreexexd  16248  lgsquadlem2  25040  elimifd  29250  elim2ifim  29252  iocinif  29428  hasheuni  29970  voliune  30115  volfiniune  30116  bnj1304  30651  fvresval  31422  wl-cases2-dnf  32966  cnambfre  33129  tsim1  33608  rp-isfinite6  37384  or3or  37840  uunT1  38528  onfrALTVD  38649  ax6e2ndeqVD  38667  ax6e2ndeqALT  38689  testable  41879
  Copyright terms: Public domain W3C validator