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	⊢ ( 𝜑 ∨ ¬ 𝜑 )