Theorem exmid 907

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 23	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	orri 875	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  exmidd  908  pm5.62  1036  pm5.63  1037  pm4.83  1042  cases  1058  xpima  6182  fvresval  7358  ssfi  9158  ixxun  13389  trclfvg  15054  mreexexd  17705  lgsquadlem2  27526  numclwwlk3lem2  30716  elimifd  32870  elim2ifim  32872  iocinif  33107  hasheuni  34456  voliune  34600  volfiniune  34601  bnj1304  35188  wl-cases2-dnf  38148  cnambfre  38300  tsim1  38760  rp-isfinite6  44227  or3or  44732  uunT1  45471  onfrALTVD  45582  ax6e2ndeqVD  45600  ax6e2ndeqALT  45622  testable  50583