Theorem exmid 894

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

Syntax hints:  ¬ wn 3   ∨ wo 847

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 848

This theorem is referenced by:  exmidd  895  pm5.62  1020  pm5.63  1021  pm4.83  1026  cases  1042  xpima  6171  fvresval  7351  ssfi  9187  ixxun  13378  trclfvg  15034  mreexexd  17660  lgsquadlem2  27344  numclwwlk3lem2  30365  elimifd  32524  elim2ifim  32526  iocinif  32758  hasheuni  34116  voliune  34260  volfiniune  34261  bnj1304  34850  wl-cases2-dnf  37530  cnambfre  37692  tsim1  38154  rp-isfinite6  43542  or3or  44047  uunT1  44804  onfrALTVD  44915  ax6e2ndeqVD  44933  ax6e2ndeqALT  44955  testable  49664