antnestlaw2

Description: A law of nested antecedents. (Contributed by Adrian Ducourtial, 5-Dec-2025)

		Ref	Expression
	Assertion	antnestlaw2	$⊢ (((φ \to ψ) \to ψ) \to χ) \leftrightarrow (((φ \to χ) \to ψ) \to χ)$

Proof

Step	Hyp	Ref	Expression
1		pm2.27	$⊢ φ \to ((φ \to ψ) \to ψ)$
2	1	a1d	$⊢ φ \to (\neg (((φ \to χ) \to ψ) \to χ) \to ((φ \to ψ) \to ψ))$
3		pm2.21	$⊢ \neg φ \to (φ \to χ)$
4	3	a1d	$⊢ \neg φ \to (\neg (((φ \to χ) \to ψ) \to χ) \to (φ \to χ))$
5		simplim	$⊢ \neg (((φ \to χ) \to ψ) \to χ) \to ((φ \to χ) \to ψ)$
6	4 5	sylcom	$⊢ \neg φ \to (\neg (((φ \to χ) \to ψ) \to χ) \to ψ)$
7	6	a1dd	$⊢ \neg φ \to (\neg (((φ \to χ) \to ψ) \to χ) \to ((φ \to ψ) \to ψ))$
8	2 7	pm2.61i	$⊢ \neg (((φ \to χ) \to ψ) \to χ) \to ((φ \to ψ) \to ψ)$
9		conax1	$⊢ \neg (((φ \to χ) \to ψ) \to χ) \to \neg χ$
10	8 9	jcnd	$⊢ \neg (((φ \to χ) \to ψ) \to χ) \to \neg (((φ \to ψ) \to ψ) \to χ)$
11	10	con4i	$⊢ (((φ \to ψ) \to ψ) \to χ) \to (((φ \to χ) \to ψ) \to χ)$
12		conax1	$⊢ \neg (((φ \to ψ) \to ψ) \to χ) \to \neg χ$
13		con3	$⊢ (φ \to χ) \to (\neg χ \to \neg φ)$
14	12 13	syl5com	$⊢ \neg (((φ \to ψ) \to ψ) \to χ) \to ((φ \to χ) \to \neg φ)$
15		pm2.21	$⊢ \neg φ \to (φ \to ψ)$
16	14 15	syl6	$⊢ \neg (((φ \to ψ) \to ψ) \to χ) \to ((φ \to χ) \to (φ \to ψ))$
17		pm2.521g2	$⊢ \neg (((φ \to ψ) \to ψ) \to χ) \to ((φ \to χ) \to ((φ \to ψ) \to ψ))$
18	16 17	mpdd	$⊢ \neg (((φ \to ψ) \to ψ) \to χ) \to ((φ \to χ) \to ψ)$
19		jcn	$⊢ ((φ \to χ) \to ψ) \to (\neg χ \to \neg (((φ \to χ) \to ψ) \to χ))$
20	19	a1i	$⊢ \neg (((φ \to ψ) \to ψ) \to χ) \to (((φ \to χ) \to ψ) \to (\neg χ \to \neg (((φ \to χ) \to ψ) \to χ)))$
21	18 20	mpd	$⊢ \neg (((φ \to ψ) \to ψ) \to χ) \to (\neg χ \to \neg (((φ \to χ) \to ψ) \to χ))$
22	12 21	mpd	$⊢ \neg (((φ \to ψ) \to ψ) \to χ) \to \neg (((φ \to χ) \to ψ) \to χ)$
23	22	con4i	$⊢ (((φ \to χ) \to ψ) \to χ) \to (((φ \to ψ) \to ψ) \to χ)$
24	11 23	impbii	$⊢ (((φ \to ψ) \to ψ) \to χ) \leftrightarrow (((φ \to χ) \to ψ) \to χ)$

Metamath Proof Explorer

Theorem antnestlaw2

Proof