{
  "citations" : [ {
    "textCitation" : "[See exmid on Metamath](http://us.metamath.org/mpegif/exmid.html)"
  } ],
  "names" : [ "exmid" ],
  "language" : "METAMATH_SET_MM",
  "lookupTerms" : [ "#T_wph", "#T_wo", "#T_wn", "#T_wph" ],
  "metaLanguage" : "METAMATH",
  "remarks" : " 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.  In intuitionistic logic, if this statement is true for some ` ph ` , then ` ph ` is decideable.  (Contributed by NM, 29-Dec-1992.) ",
  "statement" : "exmid $p |- ( ph \\/ -. ph ) $."
}