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  7368  ssfi  9191  ixxun  13495  trclfvg  15173  mreexexd  17827  lgsquadlem2  27713  numclwwlk3lem2  30990  cgrainag  33065  elimifd  33186  elim2ifim  33188  iocinif  33419  hasheuni  34763  voliune  34908  volfiniune  34909  bnj1304  35495  wl-cases2-dnf  38537  cnambfre  38679  tsim1  39155  rp-isfinite6  44612  or3or  45116  uunT1  45855  onfrALTVD  45966  ax6e2ndeqVD  45984  ax6e2ndeqALT  46006  testable  51106