Theorem exmid 431

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 decideable. (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 391	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∨ wo 383

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 197  df-or 385

This theorem is referenced by:  exmidd  432  pm5.62  958  pm5.63  959  pm4.83  970  cases  992  4exmidOLD  998  xpima  5576  ixxun  12191  trclfvg  13756  mreexexd  16308  lgsquadlem2  25106  elimifd  29362  elim2ifim  29364  iocinif  29543  hasheuni  30147  voliune  30292  volfiniune  30293  bnj1304  30890  fvresval  31665  wl-cases2-dnf  33295  cnambfre  33458  tsim1  33937  rp-isfinite6  37864  or3or  38319  uunT1  39007  onfrALTVD  39127  ax6e2ndeqVD  39145  ax6e2ndeqALT  39167  testable  42546