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	$⊢ ((((φ \to ψ) \to χ) \to φ) \to χ) \to χ$

Proof

Step	Hyp	Ref	Expression
1		bj-nnclav	$⊢ (((((φ \to ψ) \to χ) \to φ) \to χ) \to (((φ \to ψ) \to χ) \to φ)) \to (((((φ \to ψ) \to χ) \to φ) \to χ) \to χ)$
2		ax-1	$⊢ χ \to ((φ \to ψ) \to χ)$
3	2	imim2i	$⊢ ((((φ \to ψ) \to χ) \to φ) \to χ) \to ((((φ \to ψ) \to χ) \to φ) \to ((φ \to ψ) \to χ))$
4		peirce	$⊢ ((((φ \to ψ) \to χ) \to φ) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)$
5	3 4	syl	$⊢ ((((φ \to ψ) \to χ) \to φ) \to χ) \to ((φ \to ψ) \to χ)$
6		imim2	$⊢ (χ \to φ) \to (((φ \to ψ) \to χ) \to ((φ \to ψ) \to φ))$
7		peirce	$⊢ ((φ \to ψ) \to φ) \to φ$
8	5 6 7	syl56	$⊢ (χ \to φ) \to (((((φ \to ψ) \to χ) \to φ) \to χ) \to φ)$
9	8	a1dd	$⊢ (χ \to φ) \to (((((φ \to ψ) \to χ) \to φ) \to χ) \to (((φ \to ψ) \to χ) \to φ))$
10	1 9	syl11	$⊢ ((((φ \to ψ) \to χ) \to φ) \to χ) \to ((χ \to φ) \to χ)$
11		peirce	$⊢ ((χ \to φ) \to χ) \to χ$
12	10 11	syl	$⊢ ((((φ \to ψ) \to χ) \to φ) \to χ) \to χ$

Metamath Proof Explorer

Theorem bj-peircestab

Proof