Theorem exmid 892

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

Syntax hints:  ¬ wn 3   ∨ wo 844

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 845

This theorem is referenced by:  exmidd  893  pm5.62  1016  pm5.63  1017  pm4.83  1022  cases  1038  xpima  6006  ixxun  12742  trclfvg  14366  mreexexd  16911  lgsquadlem2  25965  numclwwlk3lem2  28169  elimifd  30310  elim2ifim  30312  iocinif  30530  hasheuni  31454  voliune  31598  volfiniune  31599  bnj1304  32201  fvresval  33123  wl-cases2-dnf  34917  cnambfre  35105  tsim1  35568  rp-isfinite6  40226  or3or  40724  uunT1  41486  onfrALTVD  41597  ax6e2ndeqVD  41615  ax6e2ndeqALT  41637  testable  45328