Theorem exmid 895

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

Syntax hints:  ¬ wn 3   ∨ wo 848

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 849

This theorem is referenced by:  exmidd  896  pm5.62  1021  pm5.63  1022  pm4.83  1027  cases  1043  xpima  6146  fvresval  7313  ssfi  9107  ixxun  13314  trclfvg  14977  mreexexd  17614  lgsquadlem2  27344  numclwwlk3lem2  30454  elimifd  32613  elim2ifim  32615  iocinif  32854  hasheuni  34229  voliune  34373  volfiniune  34374  bnj1304  34961  wl-cases2-dnf  37837  cnambfre  37989  tsim1  38451  rp-isfinite6  43945  or3or  44450  uunT1  45206  onfrALTVD  45317  ax6e2ndeqVD  45335  ax6e2ndeqALT  45357  testable  50275