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

Theorem peircedc 831
 Description: Peirce's theorem for a decidable proposition. This odd-looking theorem can be seen as an alternative to exmiddc 755, condc 760, or notnotrdc 762 in the sense of expressing the "difference" between an intuitionistic system of propositional calculus and a classical system. In intuitionistic logic, it only holds for decidable propositions. (Contributed by Jim Kingdon, 3-Jul-2018.)
Assertion
Ref Expression
peircedc (DECID 𝜑 → (((𝜑𝜓) → 𝜑) → 𝜑))

Proof of Theorem peircedc
StepHypRef Expression
1 df-dc 754 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
2 ax-1 5 . . 3 (𝜑 → (((𝜑𝜓) → 𝜑) → 𝜑))
3 pm2.21 557 . . . . 5 𝜑 → (𝜑𝜓))
43imim1i 58 . . . 4 (((𝜑𝜓) → 𝜑) → (¬ 𝜑𝜑))
54com12 30 . . 3 𝜑 → (((𝜑𝜓) → 𝜑) → 𝜑))
62, 5jaoi 646 . 2 ((𝜑 ∨ ¬ 𝜑) → (((𝜑𝜓) → 𝜑) → 𝜑))
71, 6sylbi 118 1 (DECID 𝜑 → (((𝜑𝜓) → 𝜑) → 𝜑))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 639  DECID wdc 753 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in2 555  ax-io 640 This theorem depends on definitions:  df-bi 114  df-dc 754 This theorem is referenced by:  looinvdc  832  exmoeudc  1979
 Copyright terms: Public domain W3C validator