Theorem exmid 891

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

Syntax hints:  ¬ wn 3   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  exmidd  892  pm5.62  1015  pm5.63  1016  pm4.83  1021  cases  1037  xpima  6039  ixxun  12755  trclfvg  14375  mreexexd  16919  lgsquadlem2  25957  numclwwlk3lem2  28163  elimifd  30298  elim2ifim  30300  iocinif  30504  hasheuni  31344  voliune  31488  volfiniune  31489  bnj1304  32091  fvresval  33010  wl-cases2-dnf  34767  cnambfre  34955  tsim1  35423  rp-isfinite6  39904  or3or  40391  uunT1  41134  onfrALTVD  41245  ax6e2ndeqVD  41263  ax6e2ndeqALT  41285  testable  44921