Theorem exmid 892

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

Syntax hints:  ¬ wn 3   ∨ wo 845

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 206  df-or 846

This theorem is referenced by:  exmidd  893  pm5.62  1016  pm5.63  1017  pm4.83  1022  cases  1040  xpima  6186  fvresval  7363  ssfi  9196  ixxun  13372  trclfvg  14995  mreexexd  17628  lgsquadlem2  27345  numclwwlk3lem2  30251  elimifd  32392  elim2ifim  32394  iocinif  32610  hasheuni  33791  voliune  33935  volfiniune  33936  bnj1304  34537  wl-cases2-dnf  37066  cnambfre  37228  tsim1  37690  rp-isfinite6  43030  or3or  43535  uunT1  44301  onfrALTVD  44412  ax6e2ndeqVD  44430  ax6e2ndeqALT  44452  testable  48361