Theorem dcfrompeirce 1472

Description: The decidability of a proposition 𝜒 follows from a suitable instance of Peirce's law. Therefore, if we were to introduce Peirce's law as a general principle (without the decidability condition in peircedc 918), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since Perice's law is itself classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)

Hypotheses

Ref	Expression
dcfrompeirce.1	⊢ (𝜑 ↔ (𝜒 ∨ ¬ 𝜒))
dcfrompeirce.2	⊢ (𝜓 ↔ ⊥)
dcfrompeirce.3	⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)

Assertion

Ref	Expression
dcfrompeirce	⊢ DECID 𝜒

Proof of Theorem dcfrompeirce

Step	Hyp	Ref	Expression
1		pm2.67-2 717	. . . . 5 ⊢ (((𝜒 ∨ ¬ 𝜒) → ⊥) → (𝜒 → ⊥))
2		dfnot 1393	. . . . 5 ⊢ (¬ 𝜒 ↔ (𝜒 → ⊥))
3	1, 2	sylibr 134	. . . 4 ⊢ (((𝜒 ∨ ¬ 𝜒) → ⊥) → ¬ 𝜒)
4	3	olcd 738	. . 3 ⊢ (((𝜒 ∨ ¬ 𝜒) → ⊥) → (𝜒 ∨ ¬ 𝜒))
5		dcfrompeirce.3	. . . 4 ⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
6		dcfrompeirce.1	. . . . . 6 ⊢ (𝜑 ↔ (𝜒 ∨ ¬ 𝜒))
7		dcfrompeirce.2	. . . . . 6 ⊢ (𝜓 ↔ ⊥)
8	6, 7	imbi12i 239	. . . . 5 ⊢ ((𝜑 → 𝜓) ↔ ((𝜒 ∨ ¬ 𝜒) → ⊥))
9	8, 6	imbi12i 239	. . . 4 ⊢ (((𝜑 → 𝜓) → 𝜑) ↔ (((𝜒 ∨ ¬ 𝜒) → ⊥) → (𝜒 ∨ ¬ 𝜒)))
10	5, 9, 6	3imtr3i 200	. . 3 ⊢ ((((𝜒 ∨ ¬ 𝜒) → ⊥) → (𝜒 ∨ ¬ 𝜒)) → (𝜒 ∨ ¬ 𝜒))
11	4, 10	ax-mp 5	. 2 ⊢ (𝜒 ∨ ¬ 𝜒)
12		df-dc 839	. 2 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
13	11, 12	mpbir 146	1 ⊢ DECID 𝜒

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

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  df-tru 1378  df-fal 1381

This theorem is referenced by: (None)