Theorem exmid 655

Description: Law of excluded middle, also called the principle of tertium 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.

Assertion

Ref	Expression
exmid	|- (ph \/ -. ph)

Proof of Theorem exmid

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

Syntax hints:  -. wn 2   \/ wo 222

This theorem is referenced by:  pm3.24 658  pm5.62 733  pm4.83 740  elimif 2374  mapdom2 4494

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

This theorem depends on definitions:  df-bi 147  df-or 224

Copyright terms: Public domain