Theorem exmid 494

Description: Law of excluded middle. 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.

Assertion

Ref	Expression
exmid	⊢ (φ ∨ ¬ φ)

Proof of Theorem exmid

Step	Hyp	Ref	Expression
1		id 9	. 2 ⊢ (¬ φ → ¬ φ)
2	1	orri 201	1 ⊢ (φ ∨ ¬ φ)

Syntax hints:  ¬ wn 1   ∨ wo 195

This theorem is referenced by:  pm3.24 496  sbc2or 1454  mapdom2 3389

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197

metamath.org