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

Theorem exmid 413
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 374 1  |-  ( ph  \/  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    \/ wo 366
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 185  df-or 368
This theorem is referenced by:  exmidd  414  pm5.62  921  pm5.63  922  pm4.83  927  4exmid  937  cases  968  exmidneOLD  2588  xpima  5359  ixxun  11466  trclfvg  12853  lgsquadlem2  23747  cusgrasizeindslem2  24595  ifbieq12d2  27545  elimifd  27546  elim2ifim  27548  iocinif  27745  hasheuni  28233  voliune  28357  volfiniune  28358  fvresval  29363  wl-cases2-dnf  30135  cnambfre  30228  tsim1  30703  testable  33549  uunT1  33917  onfrALTVD  34038  ax6e2ndeqVD  34056  ax6e2ndeqALT  34078  bnj1304  34225  rp-isfinite6  38173
  Copyright terms: Public domain W3C validator