bj-peircestab

Description: Over minimal implicational calculus, Peirce's law implies the double negation of the stability of any proposition (that is the interpretation when F. is substitued for ps ). (Contributed by BJ, 30-Nov-2023) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	bj-peircestab	$⊢ ((((φ \to ψ) \to ψ) \to φ) \to ψ) \to ψ$

Proof

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

Metamath Proof Explorer

Theorem bj-peircestab

Proof