Theorem exmid 891

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

Syntax hints:  ¬ wn 3   ∨ wo 843

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 844

This theorem is referenced by:  exmidd  892  pm5.62  1015  pm5.63  1016  pm4.83  1021  cases  1039  xpima  6074  ssfi  8918  ixxun  13024  trclfvg  14654  mreexexd  17274  lgsquadlem2  26434  numclwwlk3lem2  28649  elimifd  30787  elim2ifim  30789  iocinif  31004  hasheuni  31953  voliune  32097  volfiniune  32098  bnj1304  32699  fvresval  33647  wl-cases2-dnf  35598  cnambfre  35752  tsim1  36215  rp-isfinite6  41023  or3or  41520  uunT1  42289  onfrALTVD  42400  ax6e2ndeqVD  42418  ax6e2ndeqALT  42440  testable  46390