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  6169  fvresval  7347  ssfi  9182  ixxun  13370  trclfvg  15023  mreexexd  17647  lgsquadlem2  27330  numclwwlk3lem2  30299  elimifd  32458  elim2ifim  32460  iocinif  32695  hasheuni  34045  voliune  34189  volfiniune  34190  bnj1304  34779  wl-cases2-dnf  37459  cnambfre  37621  tsim1  38083  rp-isfinite6  43474  or3or  43979  uunT1  44738  onfrALTVD  44849  ax6e2ndeqVD  44867  ax6e2ndeqALT  44889  testable  49505