Theorem exmid 430

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

Syntax hints:  ¬ wn 3   ∨ wo 382

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 196  df-or 384

This theorem is referenced by:  exmidd  431  pm5.62  960  pm5.63  961  pm4.83  966  4exmid  977  cases  1004  xpima  5495  ixxun  12062  trclfvg  13604  mreexexd  16131  lgsquadlem2  24906  cusgrasizeindslem1  26002  elimifd  28746  elim2ifim  28748  iocinif  28933  hasheuni  29474  voliune  29619  volfiniune  29620  bnj1304  30144  fvresval  30911  wl-cases2-dnf  32474  cnambfre  32628  tsim1  33107  rp-isfinite6  36883  or3or  37339  uunT1  38028  onfrALTVD  38149  ax6e2ndeqVD  38167  ax6e2ndeqALT  38189  testable  42355