Theorem exmid 894

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

Syntax hints:  ¬ wn 3   ∨ wo 847

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 848

This theorem is referenced by:  exmidd  895  pm5.62  1020  pm5.63  1021  pm4.83  1026  cases  1042  xpima  6129  fvresval  7292  ssfi  9082  ixxun  13258  trclfvg  14919  mreexexd  17551  lgsquadlem2  27317  numclwwlk3lem2  30359  elimifd  32518  elim2ifim  32520  iocinif  32759  hasheuni  34093  voliune  34237  volfiniune  34238  bnj1304  34826  wl-cases2-dnf  37545  cnambfre  37707  tsim1  38169  rp-isfinite6  43550  or3or  44055  uunT1  44811  onfrALTVD  44922  ax6e2ndeqVD  44940  ax6e2ndeqALT  44962  testable  49831