Theorem bj-stdc 14052

Description: Decidability of a proposition is stable if and only if that proposition is decidable. In particular, the assumption that every formula is stable implies that every formula is decidable, hence classical logic. (Contributed by BJ, 9-Oct-2019.)

Assertion

Ref	Expression
bj-stdc	⊢ (STAB DECID 𝜑 ↔ DECID 𝜑)

Proof of Theorem bj-stdc

Step	Hyp	Ref	Expression
1		nndc 851	. 2 ⊢ ¬ ¬ DECID 𝜑
2		bj-nnbist 14036	. 2 ⊢ (¬ ¬ DECID 𝜑 → (STAB DECID 𝜑 ↔ DECID 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (STAB DECID 𝜑 ↔ DECID 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 105  STAB wstab 830  DECID wdc 834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709

This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835

This theorem is referenced by: (None)