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

Theorem stdcn 832
 Description: A formula is stable if and only if the decidability of its negation implies its decidability. Note that the right-hand side of this biconditional is the converse of dcn 827. (Contributed by BJ, 18-Nov-2023.)
Assertion
Ref Expression
stdcn (STAB 𝜑 ↔ (DECID ¬ 𝜑DECID 𝜑))

Proof of Theorem stdcn
StepHypRef Expression
1 stdcndc 830 . . . 4 ((STAB 𝜑DECID ¬ 𝜑) ↔ DECID 𝜑)
21biimpi 119 . . 3 ((STAB 𝜑DECID ¬ 𝜑) → DECID 𝜑)
32ex 114 . 2 (STAB 𝜑 → (DECID ¬ 𝜑DECID 𝜑))
4 olc 700 . . . . 5 (¬ ¬ 𝜑 → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
54imim1i 60 . . . 4 (((¬ 𝜑 ∨ ¬ ¬ 𝜑) → (𝜑 ∨ ¬ 𝜑)) → (¬ ¬ 𝜑 → (𝜑 ∨ ¬ 𝜑)))
6 orel2 715 . . . 4 (¬ ¬ 𝜑 → ((𝜑 ∨ ¬ 𝜑) → 𝜑))
75, 6sylcom 28 . . 3 (((¬ 𝜑 ∨ ¬ ¬ 𝜑) → (𝜑 ∨ ¬ 𝜑)) → (¬ ¬ 𝜑𝜑))
8 df-dc 820 . . . 4 (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
9 df-dc 820 . . . 4 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
108, 9imbi12i 238 . . 3 ((DECID ¬ 𝜑DECID 𝜑) ↔ ((¬ 𝜑 ∨ ¬ ¬ 𝜑) → (𝜑 ∨ ¬ 𝜑)))
11 df-stab 816 . . 3 (STAB 𝜑 ↔ (¬ ¬ 𝜑𝜑))
127, 10, 113imtr4i 200 . 2 ((DECID ¬ 𝜑DECID 𝜑) → STAB 𝜑)
133, 12impbii 125 1 (STAB 𝜑 ↔ (DECID ¬ 𝜑DECID 𝜑))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697  STAB wstab 815  DECID wdc 819 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698 This theorem depends on definitions:  df-bi 116  df-stab 816  df-dc 820 This theorem is referenced by:  dcnn  833
 Copyright terms: Public domain W3C validator