Theorem bj-peircestab 34733

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 34734). (Contributed by BJ, 30-Nov-2023.) Axiom ax-3 8 is only used through Peirce's law peirce 201. (Proof modification is discouraged.)

Assertion

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

Proof of Theorem bj-peircestab

Step	Hyp	Ref	Expression
1		bj-nnclav 34726	. . 3 ⊢ ((((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → (((𝜑 → 𝜓) → 𝜒) → 𝜑)) → (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒))
2		ax-1 6	. . . . . . 7 ⊢ (𝜒 → ((𝜑 → 𝜓) → 𝜒))
3	2	imim2i 16	. . . . . 6 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → ((((𝜑 → 𝜓) → 𝜒) → 𝜑) → ((𝜑 → 𝜓) → 𝜒)))
4		peirce 201	. . . . . 6 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → ((𝜑 → 𝜓) → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))
5	3, 4	syl 17	. . . . 5 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → ((𝜑 → 𝜓) → 𝜒))
6		imim2 58	. . . . 5 ⊢ ((𝜒 → 𝜑) → (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → 𝜓) → 𝜑)))
7		peirce 201	. . . . 5 ⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
8	5, 6, 7	syl56 36	. . . 4 ⊢ ((𝜒 → 𝜑) → (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜑))
9	8	a1dd 50	. . 3 ⊢ ((𝜒 → 𝜑) → (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → (((𝜑 → 𝜓) → 𝜒) → 𝜑)))
10	1, 9	syl11 33	. 2 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → ((𝜒 → 𝜑) → 𝜒))
11		peirce 201	. 2 ⊢ (((𝜒 → 𝜑) → 𝜒) → 𝜒)
12	10, 11	syl 17	1 ⊢ (((((𝜑 → 𝜓) → 𝜒) → 𝜑) → 𝜒) → 𝜒)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by: (None)