MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exmid 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  2573  elimif  3728  xpima  5272  ixxun  10888  lgsquadlem2  21092  cusgrasizeindslem2  21436  ifbieq12d2  23955  elimifd  23957  elim2if  23958  elim2ifim  23959  iocinif  24097  hasheuni  24428  voliune  24538  volfiniune  24539  fvresval  25337  cnambfre  26154  uunT1  28601  onfrALTVD  28712  a9e2ndeqVD  28730  a9e2ndeqALT  28753  bnj1304  28897
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