Theorem bj-peircestab 37342

Description: Over minimal implicational calculus, Peirce's law implies the double negation of the stability of any formula (that is the interpretation when ⊥ is substituted for 𝜓 and for 𝜒). Therefore, the double negation of the stability of any formula is provable in classical refutability calculus. It is also provable in intuitionistic calculus (see iset.mm/bj-nnst) but it is not provable in minimal calculus (see bj-stabpeirce 37343). (Contributed by BJ, 30-Nov-2023.) Axiom ax-3 8 is only used through Peirce's law peirce 205. (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-peircestab	⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒)

Proof of Theorem bj-peircestab

Step	Hyp	Ref	Expression
1		bj-nnclav 37333	. . 3 ⊢ ((((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → (((𝜑 → 𝜓) → 𝜒) → 𝜑)) → (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒))
2		ax-1 6	. . . . . . 7 ⊢ (𝜒 → ((𝜑 → 𝜓) → 𝜒))
3	2	imim2i 17	. . . . . 6 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → ((((𝜑 → 𝜓) → 𝜒) → 𝜑) → ((𝜑 → 𝜓) → 𝜒)))
4		peirce 205	. . . . . 6 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))
5	3, 4	syl 18	. . . . 5 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → ((𝜑 → 𝜓) → 𝜒))
6		imim2 59	. . . . 5 ⊢ ((𝜒 → 𝜑) → (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜑)))
7		peirce 205	. . . . 5 ⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
8	5, 6, 7	syl56 37	. . . 4 ⊢ ((𝜒 → 𝜑) → (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜑))
9	8	a1dd 51	. . 3 ⊢ ((𝜒 → 𝜑) → (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → (((𝜑 → 𝜓) → 𝜒) → 𝜑)))
10	1, 9	syl11 34	. 2 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → ((𝜒 → 𝜑) → 𝜒))
11		peirce 205	. 2 ⊢ (((𝜒 → 𝜑) → 𝜒) → 𝜒)
12	10, 11	syl 18	1 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by: (None)