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

Theorem exmid 405
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 20 . 2  |-  ( -. 
ph  ->  -.  ph )
21orri 366 1  |-  ( ph  \/  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 358
This theorem is referenced by:  exmidd  406  pm5.62  890  pm5.63  891  pm4.83  896  4exmid  906  jaoi2  934  exmidne  2607  elimif  3768  xpima  5313  ixxun  10932  lgsquadlem2  21139  cusgrasizeindslem2  21483  ifbieq12d2  24002  elimifd  24004  elim2if  24005  elim2ifim  24006  iocinif  24144  hasheuni  24475  voliune  24585  volfiniune  24586  fvresval  25391  cnambfre  26255  uunT1  28892  onfrALTVD  29003  a9e2ndeqVD  29021  a9e2ndeqALT  29043  bnj1304  29191
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 178  df-or 360
  Copyright terms: Public domain W3C validator