Theorem peirce2exclmid-P4.41b 513

Description: Law of Excluded Middle from Peirce's Law. †

The hypothesis is a special case of Peirce's Law.

Hypothesis

Ref	Expression
peirce2exclmid-P4.41b.1	⊢ ((((𝜑 ∨ ¬ 𝜑) → ⊥) → (𝜑 ∨ ¬ 𝜑)) → (𝜑 ∨ ¬ 𝜑))

Assertion

Ref	Expression
peirce2exclmid-P4.41b	⊢ (𝜑 ∨ ¬ 𝜑)

Proof of Theorem peirce2exclmid-P4.41b

Step	Hyp	Ref	Expression
1		norer-P4.2b.CL 372	. . . 4 ⊢ (¬ (𝜑 ∨ ¬ 𝜑) → ¬ 𝜑)
2	1	ndoril-P3.10 175	. . 3 ⊢ (¬ (𝜑 ∨ ¬ 𝜑) → (𝜑 ∨ ¬ 𝜑))
3		falseie-P4.22b 445	. . . . . 6 ⊢ (((𝜑 ∨ ¬ 𝜑) → ⊥) ↔ ¬ (𝜑 ∨ ¬ 𝜑))
4	3	bisym-P3.33b.RC 299	. . . . 5 ⊢ (¬ (𝜑 ∨ ¬ 𝜑) ↔ ((𝜑 ∨ ¬ 𝜑) → ⊥))
5	4	subiml-P3.40a.RC 326	. . . 4 ⊢ ((¬ (𝜑 ∨ ¬ 𝜑) → (𝜑 ∨ ¬ 𝜑)) ↔ (((𝜑 ∨ ¬ 𝜑) → ⊥) → (𝜑 ∨ ¬ 𝜑)))
6	5	rcp-NDBIEF0 240	. . 3 ⊢ ((¬ (𝜑 ∨ ¬ 𝜑) → (𝜑 ∨ ¬ 𝜑)) → (((𝜑 ∨ ¬ 𝜑) → ⊥) → (𝜑 ∨ ¬ 𝜑)))
7	2, 6	rcp-NDIME0 228	. 2 ⊢ (((𝜑 ∨ ¬ 𝜑) → ⊥) → (𝜑 ∨ ¬ 𝜑))
8		peirce2exclmid-P4.41b.1	. 2 ⊢ ((((𝜑 ∨ ¬ 𝜑) → ⊥) → (𝜑 ∨ ¬ 𝜑)) → (𝜑 ∨ ¬ 𝜑))
9	7, 8	rcp-NDIME0 228	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wff-neg 9   → wff-imp 10   ∨ wff-or 144  ⊥wff-false 157

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-false-D2.5 158

This theorem is referenced by: (None)