exmid Show Code edit
## Law of excluded middle
##
## Law of excluded middle, also called the principle of tertium non datur.
## 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.
##
thm (exmid () () (\/ ph (-. ph)) (-. ph) id orri)
(\/ ph (-. ph))
edit