Theorem exmid 900

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. In intuitionistic logic, if this statement is true for some 𝜑, then 𝜑 is decidable. (Contributed by NM, 29-Dec-1992.)

Assertion

Ref	Expression
exmid	⊢ (𝜑 ∨ ¬ 𝜑)

Proof of Theorem exmid

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	orri 868	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∨ wo 853

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

This theorem depends on definitions:  df-bi 208  df-or 854

This theorem is referenced by:  exmidd  901  pm5.62  1026  pm5.63  1027  pm4.83  1032  cases  1048  xpima  6140  fvresval  7309  ssfi  9104  ixxun  13312  trclfvg  14975  mreexexd  17612  lgsquadlem2  27369  numclwwlk3lem2  30479  elimifd  32638  elim2ifim  32640  iocinif  32880  hasheuni  34276  voliune  34420  volfiniune  34421  bnj1304  35008  wl-cases2-dnf  37890  cnambfre  38042  tsim1  38504  rp-isfinite6  43969  or3or  44474  uunT1  45230  onfrALTVD  45341  ax6e2ndeqVD  45359  ax6e2ndeqALT  45381  testable  50297