ILE Home 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