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 206  df-or 847
This theorem is referenced by:  exmidd  895  pm5.62  1018  pm5.63  1019  pm4.83  1024  cases  1042  xpima  6182  fvresval  7355  ssfi  9173  ixxun  13340  trclfvg  14962  mreexexd  17592  lgsquadlem2  26884  numclwwlk3lem2  29637  elimifd  31775  elim2ifim  31777  iocinif  31992  hasheuni  33083  voliune  33227  volfiniune  33228  bnj1304  33830  wl-cases2-dnf  36381  cnambfre  36536  tsim1  36998  rp-isfinite6  42269  or3or  42774  uunT1  43541  onfrALTVD  43652  ax6e2ndeqVD  43670  ax6e2ndeqALT  43692  testable  47847
  Copyright terms: Public domain W3C validator