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  2465  rabxm  3490  elimif  3607  ixxun  10688  lgsquadlem2  20610  ifbieq12d2  23165  elimifd  23167  elim2if  23168  elim2ifim  23169  xpima  23217  iocinif  23289  hasheuni  23468  fvresval  24194  condis  25045  condisd  25046  altdftru  25051  pdiveql  26271  jaoi2  28176  uunT1  28869  onfrALTVD  28983  a9e2ndeqVD  29001  a9e2ndeqALT  29024  bnj1304  29168  a12study4  29739
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