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	|- (ph \/ -. ph)

Proof of Theorem exmid

Step	Hyp	Ref	Expression
1		id 9	. 2 |- (-. ph -> -. ph)
2	1	orri 201	1 |- (ph \/ -. ph)

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