MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exmid Structured version   Visualization 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 22 . 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  935  pm5.63  936  pm4.83  941  4exmid  951  cases  983  xpima  5282  ixxun  11658  trclfvg  13091  lgsquadlem2  24295  cusgrasizeindslem2  25214  ifbieq12d2  28171  elimifd  28172  elim2ifim  28174  iocinif  28375  hasheuni  28918  voliune  29064  volfiniune  29065  bnj1304  29643  fvresval  30420  wl-cases2-dnf  31862  cnambfre  32001  tsim1  32384  rp-isfinite6  36175  uunT1  37177  onfrALTVD  37298  ax6e2ndeqVD  37316  ax6e2ndeqALT  37338  testable  40643
  Copyright terms: Public domain W3C validator