Theorem exmid 907

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

Syntax hints:  ¬ wn 3   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  exmidd  908  pm5.62  1034  pm5.63  1035  pm4.83  1040  cases  1056  xpima  6172  fvresval  7346  ssfi  9145  ixxun  13379  trclfvg  15042  mreexexd  17694  lgsquadlem2  27503  numclwwlk3lem2  30644  elimifd  32799  elim2ifim  32801  iocinif  33038  hasheuni  34392  voliune  34536  volfiniune  34537  bnj1304  35124  wl-cases2-dnf  38027  cnambfre  38179  tsim1  38641  rp-isfinite6  44106  or3or  44611  uunT1  45353  onfrALTVD  45464  ax6e2ndeqVD  45482  ax6e2ndeqALT  45504  testable  50429