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

Theorem exmid 417
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  ph, then  ph is decideable. (Contributed by NM, 29-Dec-1992.)
Assertion
Ref Expression
exmid  |-  ( ph  \/  -.  ph )

Proof of Theorem exmid
StepHypRef Expression
1 id 23 . 2  |-  ( -. 
ph  ->  -.  ph )
21orri 378 1  |-  ( ph  \/  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    \/ wo 370
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 189  df-or 372
This theorem is referenced by:  exmidd  418  pm5.62  932  pm5.63  933  pm4.83  938  4exmid  948  cases  980  exmidneOLD  2631  xpima  5296  ixxun  11653  trclfvg  13073  lgsquadlem2  24275  cusgrasizeindslem2  25194  ifbieq12d2  28155  elimifd  28156  elim2ifim  28158  iocinif  28363  hasheuni  28908  voliune  29054  volfiniune  29055  bnj1304  29633  fvresval  30409  wl-cases2-dnf  31808  cnambfre  31947  tsim1  32330  rp-isfinite6  36127  uunT1  37072  onfrALTVD  37193  ax6e2ndeqVD  37211  ax6e2ndeqALT  37233  testable  39883
  Copyright terms: Public domain W3C validator