Theorem exmid 908

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

This proof depends on syntax axioms:  ¬ wn 3   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  exmidd  909  pm5.62  1036  pm5.63  1037  pm4.83  1042  cases  1058  xpima  6179  fvresval  7365  ssfi  9171  ixxun  13418  trclfvg  15092  mreexexd  17742  lgsquadlem2  27625  numclwwlk3lem2  30872  elimifd  33026  elim2ifim  33028  iocinif  33260  hasheuni  34603  voliune  34748  volfiniune  34749  bnj1304  35336  wl-cases2-dnf  38283  cnambfre  38425  tsim1  38886  rp-isfinite6  44366  or3or  44871  uunT1  45610  onfrALTVD  45721  ax6e2ndeqVD  45739  ax6e2ndeqALT  45761  testable  50779