Theorem exmid 895

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

Syntax hints:  ¬ wn 3   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  exmidd  896  pm5.62  1021  pm5.63  1022  pm4.83  1027  cases  1043  xpima  6202  fvresval  7378  ssfi  9213  ixxun  13403  trclfvg  15054  mreexexd  17691  lgsquadlem2  27425  numclwwlk3lem2  30403  elimifd  32556  elim2ifim  32558  iocinif  32783  hasheuni  34086  voliune  34230  volfiniune  34231  bnj1304  34833  wl-cases2-dnf  37513  cnambfre  37675  tsim1  38137  rp-isfinite6  43531  or3or  44036  uunT1  44800  onfrALTVD  44911  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  testable  49319