Theorem exmid 923

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

Syntax hints:  ¬ wn 3   ∨ wo 878

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 199  df-or 879

This theorem is referenced by:  exmidd  924  pm5.62  1047  pm5.63  1048  pm4.83  1053  cases  1069  xpima  5817  ixxun  12479  trclfvg  14133  mreexexd  16661  lgsquadlem2  25519  numclwwlk3lem2  27788  elimifd  29899  elim2ifim  29901  iocinif  30079  hasheuni  30681  voliune  30826  volfiniune  30827  bnj1304  31425  fvresval  32196  wl-cases2-dnf  33833  cnambfre  33994  tsim1  34470  rp-isfinite6  38698  or3or  39152  uunT1  39827  onfrALTVD  39938  ax6e2ndeqVD  39956  ax6e2ndeqALT  39978  testable  43435