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

Theorem exmid 406
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 21 . 2  |-  ( -. 
ph  ->  -.  ph )
21orri 367 1  |-  ( ph  \/  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    \/ wo 359
This theorem is referenced by:  exmidd  407  pm5.62  891  pm5.63  892  pm4.83  897  4exmid  907  exmidne  2453  rabxm  3478  elimif  3595  ixxun  10666  lgsquadlem2  20588  fvresval  23524  condis  24340  condisd  24341  altdftru  24346  pdiveql  25567  uunT1  27823  onfrALTVD  27935  a9e2ndeqVD  27953  a9e2ndeqALT  27976  bnj1304  28119  a12study4  28384
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator