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	$$⊢\left(\phi \vee \neg \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\neg \phi \to \neg \phi$$
2	1	orri	$$⊢\left(\phi \vee \neg \phi \right)$$