Theorem antnestlaw3lem 35684

Description: Lemma for antnestlaw3 35687. (Contributed by Adrian Ducourtial, 5-Dec-2025.)

Assertion

Ref	Expression
antnestlaw3lem	⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ¬ (((𝜑 → 𝜒) → 𝜓) → 𝜓))

Proof of Theorem antnestlaw3lem

Step	Hyp	Ref	Expression
1		conax1 170	. . . . . 6 ⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ¬ 𝜒)
2		simplim 167	. . . . . 6 ⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ((𝜑 → 𝜓) → 𝜒))
3	1, 2	mtod 198	. . . . 5 ⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ¬ (𝜑 → 𝜓))
4		simplim 167	. . . . 5 ⊢ (¬ (𝜑 → 𝜓) → 𝜑)
5	3, 4	syl 17	. . . 4 ⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → 𝜑)
6	5, 1	jcnd 163	. . 3 ⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ¬ (𝜑 → 𝜒))
7	6	pm2.21d 121	. 2 ⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ((𝜑 → 𝜒) → 𝜓))
8		conax1 170	. . 3 ⊢ (¬ (𝜑 → 𝜓) → ¬ 𝜓)
9	3, 8	syl 17	. 2 ⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ¬ 𝜓)
10	7, 9	jcnd 163	1 ⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ¬ (((𝜑 → 𝜒) → 𝜓) → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  antnestlaw3  35687