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  5535  ixxun  12133  trclfvg  13690  mreexexd  16229  lgsquadlem2  25006  elimifd  29206  elim2ifim  29208  iocinif  29384  hasheuni  29925  voliune  30070  volfiniune  30071  bnj1304  30595  fvresval  31366  wl-cases2-dnf  32924  cnambfre  33087  tsim1  33566  rp-isfinite6  37342  or3or  37798  uunT1  38486  onfrALTVD  38607  ax6e2ndeqVD  38625  ax6e2ndeqALT  38647  testable  41846
  Copyright terms: Public domain W3C validator