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  6148  fvresval  7314  ssfi  9109  ixxun  13289  trclfvg  14950  mreexexd  17583  lgsquadlem2  27360  numclwwlk3lem2  30471  elimifd  32629  elim2ifim  32631  iocinif  32871  hasheuni  34262  voliune  34406  volfiniune  34407  bnj1304  34994  wl-cases2-dnf  37761  cnambfre  37913  tsim1  38375  rp-isfinite6  43868  or3or  44373  uunT1  45129  onfrALTVD  45240  ax6e2ndeqVD  45258  ax6e2ndeqALT  45280  testable  50153