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  6157  fvresval  7335  ssfi  9142  ixxun  13328  trclfvg  14987  mreexexd  17615  lgsquadlem2  27298  numclwwlk3lem2  30319  elimifd  32478  elim2ifim  32480  iocinif  32710  hasheuni  34081  voliune  34225  volfiniune  34226  bnj1304  34815  wl-cases2-dnf  37495  cnambfre  37657  tsim1  38119  rp-isfinite6  43500  or3or  44005  uunT1  44762  onfrALTVD  44873  ax6e2ndeqVD  44891  ax6e2ndeqALT  44913  testable  49779