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

Theorem exmid 404
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. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
exmid  |-  ( ph  \/  -.  ph )

Proof of Theorem exmid
StepHypRef Expression
1 id 19 . 2  |-  ( -. 
ph  ->  -.  ph )
21orri 365 1  |-  ( ph  \/  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 357
This theorem is referenced by:  exmidd  405  pm5.62  889  pm5.63  890  pm4.83  895  4exmid  905  exmidne  2452  rabxm  3477  elimif  3594  ixxun  10672  lgsquadlem2  20594  ifbieq12d2  23149  elimifd  23151  elim2if  23152  elim2ifim  23153  xpima  23202  iocinif  23274  hasheuni  23453  fvresval  24123  condis  24942  condisd  24943  altdftru  24948  pdiveql  26168  uunT1  28555  onfrALTVD  28667  a9e2ndeqVD  28685  a9e2ndeqALT  28708  bnj1304  28852  a12study4  29117
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator