Theorem dcfromnotnotr 1470

Description: The decidability of a proposition 𝜓 follows from a suitable instance of double negation elimination (DNE). Therefore, if we were to introduce DNE as a general principle (without the decidability condition in notnotrdc 847), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since DNE itself is classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)

Hypotheses

Ref	Expression
dcfromnotnotr.1	⊢ (𝜑 ↔ (𝜓 ∨ ¬ 𝜓))
dcfromnotnotr.2	⊢ (¬ ¬ 𝜑 → 𝜑)

Assertion

Ref	Expression
dcfromnotnotr	⊢ DECID 𝜓

Proof of Theorem dcfromnotnotr

Step	Hyp	Ref	Expression
1		nnexmid 854	. . 3 ⊢ ¬ ¬ (𝜓 ∨ ¬ 𝜓)
2		dcfromnotnotr.2	. . . 4 ⊢ (¬ ¬ 𝜑 → 𝜑)
3		dcfromnotnotr.1	. . . . . 6 ⊢ (𝜑 ↔ (𝜓 ∨ ¬ 𝜓))
4	3	notbii 672	. . . . 5 ⊢ (¬ 𝜑 ↔ ¬ (𝜓 ∨ ¬ 𝜓))
5	4	notbii 672	. . . 4 ⊢ (¬ ¬ 𝜑 ↔ ¬ ¬ (𝜓 ∨ ¬ 𝜓))
6	2, 5, 3	3imtr3i 200	. . 3 ⊢ (¬ ¬ (𝜓 ∨ ¬ 𝜓) → (𝜓 ∨ ¬ 𝜓))
7	1, 6	ax-mp 5	. 2 ⊢ (𝜓 ∨ ¬ 𝜓)
8		df-dc 839	. 2 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
9	7, 8	mpbir 146	1 ⊢ DECID 𝜓

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ wo 712  DECID wdc 838

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 617  ax-in2 618  ax-io 713

This theorem depends on definitions:  df-bi 117  df-dc 839

This theorem is referenced by: (None)