Theorem exmid 905

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

Syntax hints:  ¬ wn 3   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  exmidd  906  pm5.62  1031  pm5.63  1032  pm4.83  1037  cases  1053  xpima  6164  fvresval  7338  ssfi  9137  ixxun  13362  trclfvg  15025  mreexexd  17663  lgsquadlem2  27422  numclwwlk3lem2  30532  elimifd  32691  elim2ifim  32693  iocinif  32933  hasheuni  34343  voliune  34487  volfiniune  34488  bnj1304  35078  wl-cases2-dnf  37979  cnambfre  38131  tsim1  38593  rp-isfinite6  44058  or3or  44563  uunT1  45319  onfrALTVD  45430  ax6e2ndeqVD  45448  ax6e2ndeqALT  45470  testable  50385