antnestlaw3

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

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

Step	Hyp	Ref	Expression
1		antnestlaw3lem	$⊢ \neg (((φ \to χ) \to ψ) \to ψ) \to \neg (((φ \to ψ) \to χ) \to χ)$
2	1	con4i	$⊢ (((φ \to ψ) \to χ) \to χ) \to (((φ \to χ) \to ψ) \to ψ)$
3		antnestlaw3lem	$⊢ \neg (((φ \to ψ) \to χ) \to χ) \to \neg (((φ \to χ) \to ψ) \to ψ)$
4	3	con4i	$⊢ (((φ \to χ) \to ψ) \to ψ) \to (((φ \to ψ) \to χ) \to χ)$
5	2 4	impbii	$⊢ (((φ \to ψ) \to χ) \to χ) \leftrightarrow (((φ \to χ) \to ψ) \to ψ)$

Metamath Proof Explorer