Theorem antnestlaw2

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

	Ref	Expression
Assertion	antnestlaw2	⊢ ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) ↔ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.27	⊢ ( 𝜑 → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )
2	1	a1d	⊢ ( 𝜑 → ( ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) ) )
3		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜒 ) )
4	3	a1d	⊢ ( ¬ 𝜑 → ( ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) → ( 𝜑 → 𝜒 ) ) )
5		simplim	⊢ ( ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → 𝜒 ) → 𝜓 ) )
6	4 5	sylcom	⊢ ( ¬ 𝜑 → ( ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) → 𝜓 ) )
7	6	a1dd	⊢ ( ¬ 𝜑 → ( ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) ) )
8	2 7	pm2.61i	⊢ ( ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )
9		conax1	⊢ ( ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) → ¬ 𝜒 )
10	8 9	jcnd	⊢ ( ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) → ¬ ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) )
11	10	con4i	⊢ ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) → ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) )
12		conax1	⊢ ( ¬ ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) → ¬ 𝜒 )
13		con3	⊢ ( ( 𝜑 → 𝜒 ) → ( ¬ 𝜒 → ¬ 𝜑 ) )
14	12 13	syl5com	⊢ ( ¬ ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → 𝜒 ) → ¬ 𝜑 ) )
15		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) )
16	14 15	syl6	⊢ ( ¬ ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → 𝜒 ) → ( 𝜑 → 𝜓 ) ) )
17		pm2.521g2	⊢ ( ¬ ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → 𝜒 ) → ( ( 𝜑 → 𝜓 ) → 𝜓 ) ) )
18	16 17	mpdd	⊢ ( ¬ ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) → ( ( 𝜑 → 𝜒 ) → 𝜓 ) )
19		jcn	⊢ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → ( ¬ 𝜒 → ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) ) )
20	19	a1i	⊢ ( ¬ ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) → ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → ( ¬ 𝜒 → ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) ) ) )
21	18 20	mpd	⊢ ( ¬ ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) → ( ¬ 𝜒 → ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) ) )
22	12 21	mpd	⊢ ( ¬ ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) → ¬ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) )
23	22	con4i	⊢ ( ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) → ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) )
24	11 23	impbii	⊢ ( ( ( ( 𝜑 → 𝜓 ) → 𝜓 ) → 𝜒 ) ↔ ( ( ( 𝜑 → 𝜒 ) → 𝜓 ) → 𝜒 ) )