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

Syntax hints:  ¬ wn 3   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  exmidd  895  pm5.62  1018  pm5.63  1019  pm4.83  1024  cases  1042  xpima  6179  fvresval  7352  ssfi  9170  ixxun  13337  trclfvg  14959  mreexexd  17589  lgsquadlem2  26874  numclwwlk3lem2  29627  elimifd  31763  elim2ifim  31765  iocinif  31980  hasheuni  33072  voliune  33216  volfiniune  33217  bnj1304  33819  wl-cases2-dnf  36370  cnambfre  36525  tsim1  36987  rp-isfinite6  42255  or3or  42760  uunT1  43527  onfrALTVD  43638  ax6e2ndeqVD  43656  ax6e2ndeqALT  43678  testable  47801