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  6140  fvresval  7304  ssfi  9097  ixxun  13277  trclfvg  14938  mreexexd  17571  lgsquadlem2  27348  numclwwlk3lem2  30459  elimifd  32618  elim2ifim  32620  iocinif  32861  hasheuni  34242  voliune  34386  volfiniune  34387  bnj1304  34975  wl-cases2-dnf  37713  cnambfre  37865  tsim1  38327  rp-isfinite6  43755  or3or  44260  uunT1  45016  onfrALTVD  45127  ax6e2ndeqVD  45145  ax6e2ndeqALT  45167  testable  50041