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

Theorem exmid 429
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 389 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 381
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 195  df-or 383
This theorem is referenced by:  exmidd  430  pm5.62  959  pm5.63  960  pm4.83  965  4exmid  976  cases  1003  xpima  5481  ixxun  12018  trclfvg  13550  mreexexd  16077  lgsquadlem2  24823  cusgrasizeindslem1  25768  elimifd  28552  elim2ifim  28554  iocinif  28739  hasheuni  29280  voliune  29425  volfiniune  29426  bnj1304  29950  fvresval  30717  wl-cases2-dnf  32270  cnambfre  32424  tsim1  32903  rp-isfinite6  36679  or3or  37135  uunT1  37824  onfrALTVD  37945  ax6e2ndeqVD  37963  ax6e2ndeqALT  37985  testable  42311
  Copyright terms: Public domain W3C validator