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

Theorem exmid 894
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 861 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 846
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 210  df-or 847
This theorem is referenced by:  exmidd  895  pm5.62  1018  pm5.63  1019  pm4.83  1024  cases  1042  xpima  6014  ssfi  8772  ixxun  12837  trclfvg  14464  mreexexd  17022  lgsquadlem2  26117  numclwwlk3lem2  28321  elimifd  30460  elim2ifim  30462  iocinif  30677  hasheuni  31623  voliune  31767  volfiniune  31768  bnj1304  32370  fvresval  33313  wl-cases2-dnf  35294  cnambfre  35448  tsim1  35911  rp-isfinite6  40679  or3or  41177  uunT1  41938  onfrALTVD  42049  ax6e2ndeqVD  42067  ax6e2ndeqALT  42089  testable  45957
  Copyright terms: Public domain W3C validator