Metamath Proof Explorer


Theorem exmid

Description: Law of excluded middle, also called the principle oftertium 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 decidable. (Contributed by NM, 29-Dec-1992)

Ref Expression
Assertion exmid φ ¬ φ

Proof

Step Hyp Ref Expression
1 id ¬ φ ¬ φ
2 1 orri φ ¬ φ