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  6185  fvresval  7369  ssfi  9167  ixxun  13406  trclfvg  15078  mreexexd  17729  lgsquadlem2  27582  numclwwlk3lem2  30772  elimifd  32926  elim2ifim  32928  iocinif  33163  hasheuni  34506  voliune  34651  volfiniune  34652  bnj1304  35239  wl-cases2-dnf  38208  cnambfre  38360  tsim1  38820  rp-isfinite6  44285  or3or  44790  uunT1  45529  onfrALTVD  45640  ax6e2ndeqVD  45658  ax6e2ndeqALT  45680  testable  50661