Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  exmiddc GIF version

Theorem exmiddc 744
 Description: Law of excluded middle, for a decidable proposition. The law of the excluded middle is 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. The key way in which intuitionistic logic differs from classical logic is that intuitionistic logic says that excluded middle only holds for some propositions, and classical logic says that it holds for all propositions. (Contributed by Jim Kingdon, 12-May-2018.)
Assertion
Ref Expression
exmiddc (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑))

Proof of Theorem exmiddc
StepHypRef Expression
1 df-dc 743 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
21biimpi 113 1 (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 629  DECID wdc 742 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99 This theorem depends on definitions:  df-bi 110  df-dc 743 This theorem is referenced by:  stabtestimpdc  824  modc  1943  rabxmdc  3249  ifbothdc  3357  fidceq  6330  fidifsnen  6331  flqeqceilz  9160
 Copyright terms: Public domain W3C validator