Theorem exmid 717

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 73	. 2 |- (-. ph -> -. ph)
2	1	orri 248	1 |- (ph \/ -. ph)

Syntax hints:  -. wn 2   \/ wo 239

This theorem is referenced by:  pm3.24 720  pm5.62 805  pm4.83 812  exmidne 2022  elimif 3001  mapdom2 5588  bnj1119 12929  bnj1221 12996  fvresval 13841  condis 14269  condisd 14270  altdftru 14283  trtrst 14330  rabxm 15667  pcopt 16084  pleval2 16785

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 164  df-or 241

Copyright terms: Public domain