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

Theorem stdcn 842
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 837. (Contributed by BJ, 18-Nov-2023.)
Assertion
Ref Expression
stdcn (STAB 𝜑 ↔ (DECID ¬ 𝜑DECID 𝜑))

Proof of Theorem stdcn
StepHypRef Expression
1 stdcndc 840 . . . 4 ((STAB 𝜑DECID ¬ 𝜑) ↔ DECID 𝜑)
21biimpi 119 . . 3 ((STAB 𝜑DECID ¬ 𝜑) → DECID 𝜑)
32ex 114 . 2 (STAB 𝜑 → (DECID ¬ 𝜑DECID 𝜑))
4 olc 706 . . . . 5 (¬ ¬ 𝜑 → (¬ 𝜑 ∨ ¬ ¬ 𝜑))
54imim1i 60 . . . 4 (((¬ 𝜑 ∨ ¬ ¬ 𝜑) → (𝜑 ∨ ¬ 𝜑)) → (¬ ¬ 𝜑 → (𝜑 ∨ ¬ 𝜑)))
6 orel2 721 . . . 4 (¬ ¬ 𝜑 → ((𝜑 ∨ ¬ 𝜑) → 𝜑))
75, 6sylcom 28 . . 3 (((¬ 𝜑 ∨ ¬ ¬ 𝜑) → (𝜑 ∨ ¬ 𝜑)) → (¬ ¬ 𝜑𝜑))
8 df-dc 830 . . . 4 (DECID ¬ 𝜑 ↔ (¬ 𝜑 ∨ ¬ ¬ 𝜑))
9 df-dc 830 . . . 4 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
108, 9imbi12i 238 . . 3 ((DECID ¬ 𝜑DECID 𝜑) ↔ ((¬ 𝜑 ∨ ¬ ¬ 𝜑) → (𝜑 ∨ ¬ 𝜑)))
11 df-stab 826 . . 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 703  STAB wstab 825  DECID wdc 829
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 609  ax-in2 610  ax-io 704
This theorem depends on definitions:  df-bi 116  df-stab 826  df-dc 830
This theorem is referenced by:  dcnn  843  bj-charfunbi  13806
  Copyright terms: Public domain W3C validator