Theorem exmid 893

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 861	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∨ wo 846

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 207  df-or 847

This theorem is referenced by:  exmidd  894  pm5.62  1019  pm5.63  1020  pm4.83  1025  cases  1043  xpima  6213  fvresval  7394  ssfi  9240  ixxun  13423  trclfvg  15064  mreexexd  17706  lgsquadlem2  27443  numclwwlk3lem2  30416  elimifd  32566  elim2ifim  32568  iocinif  32786  hasheuni  34049  voliune  34193  volfiniune  34194  bnj1304  34795  wl-cases2-dnf  37466  cnambfre  37628  tsim1  38090  rp-isfinite6  43480  or3or  43985  uunT1  44751  onfrALTVD  44862  ax6e2ndeqVD  44880  ax6e2ndeqALT  44902  testable  48894