Theorem bj-peircestab

Description: Over minimal implicational calculus, Peirce's law implies the double negation of the stability of any formula (that is the interpretation when F. is substituted for ps and for ch ). 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 ). (Contributed by BJ, 30-Nov-2023) Axiom ax-3 is only used through Peirce's law peirce . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-peircestab	|- ( ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ch ) -> ch )

Proof

Step	Hyp	Ref	Expression
1		bj-nnclav	|- ( ( ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ch ) -> ( ( ( ph -> ps ) -> ch ) -> ph ) ) -> ( ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ch ) -> ch ) )
2		ax-1	|- ( ch -> ( ( ph -> ps ) -> ch ) )
3	2	imim2i	|- ( ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ch ) -> ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ( ( ph -> ps ) -> ch ) ) )
4		peirce	|- ( ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ( ( ph -> ps ) -> ch ) ) -> ( ( ph -> ps ) -> ch ) )
5	3 4	syl	|- ( ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ch ) -> ( ( ph -> ps ) -> ch ) )
6		imim2	|- ( ( ch -> ph ) -> ( ( ( ph -> ps ) -> ch ) -> ( ( ph -> ps ) -> ph ) ) )
7		peirce	|- ( ( ( ph -> ps ) -> ph ) -> ph )
8	5 6 7	syl56	|- ( ( ch -> ph ) -> ( ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ch ) -> ph ) )
9	8	a1dd	|- ( ( ch -> ph ) -> ( ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ch ) -> ( ( ( ph -> ps ) -> ch ) -> ph ) ) )
10	1 9	syl11	|- ( ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ch ) -> ( ( ch -> ph ) -> ch ) )
11		peirce	|- ( ( ( ch -> ph ) -> ch ) -> ch )
12	10 11	syl	|- ( ( ( ( ( ph -> ps ) -> ch ) -> ph ) -> ch ) -> ch )