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  6173  fvresval  7360  ssfi  9172  ixxun  13473  trclfvg  15148  mreexexd  17802  lgsquadlem2  27690  numclwwlk3lem2  30967  elimifd  33121  elim2ifim  33123  iocinif  33355  hasheuni  34699  voliune  34844  volfiniune  34845  bnj1304  35432  wl-cases2-dnf  38412  cnambfre  38554  tsim1  39030  rp-isfinite6  44477  or3or  44982  uunT1  45721  onfrALTVD  45832  ax6e2ndeqVD  45850  ax6e2ndeqALT  45872  testable  50882