Theorem bj-stdc 16788

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 863	. 2 ⊢ ¬ ¬ DECID 𝜑
2		bj-nnbist 16772	. 2 ⊢ (¬ ¬ DECID 𝜑 → (STAB DECID 𝜑 ↔ DECID 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (STAB DECID 𝜑 ↔ DECID 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 105  STAB wstab 842  DECID wdc 846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847

This theorem is used by: (None)