antnestlaw3lem

		Ref	Expression
	Assertion	antnestlaw3lem	$⊢ \neg (((φ \to ψ) \to χ) \to χ) \to \neg (((φ \to χ) \to ψ) \to ψ)$

Step	Hyp	Ref	Expression
1		conax1	$⊢ \neg (((φ \to ψ) \to χ) \to χ) \to \neg χ$
2		simplim	$⊢ \neg (((φ \to ψ) \to χ) \to χ) \to ((φ \to ψ) \to χ)$
3	1 2	mtod	$⊢ \neg (((φ \to ψ) \to χ) \to χ) \to \neg (φ \to ψ)$
4		simplim	$⊢ \neg (φ \to ψ) \to φ$
5	3 4	syl	$⊢ \neg (((φ \to ψ) \to χ) \to χ) \to φ$
6	5 1	jcnd	$⊢ \neg (((φ \to ψ) \to χ) \to χ) \to \neg (φ \to χ)$
7	6	pm2.21d	$⊢ \neg (((φ \to ψ) \to χ) \to χ) \to ((φ \to χ) \to ψ)$
8		conax1	$⊢ \neg (φ \to ψ) \to \neg ψ$
9	3 8	syl	$⊢ \neg (((φ \to ψ) \to χ) \to χ) \to \neg ψ$
10	7 9	jcnd	$⊢ \neg (((φ \to ψ) \to χ) \to χ) \to \neg (((φ \to χ) \to ψ) \to ψ)$

Metamath Proof Explorer