Metamath Proof Explorer

Theorem antnestlaw1

Description: A law of nested antecedents. The converse direction is a subschema of pm2.27 . (Contributed by Adrian Ducourtial, 5-Dec-2025)

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

Step	Hyp	Ref	Expression
1		pm2.21	$⊢ \neg (φ \to ψ) \to ((φ \to ψ) \to ψ)$
2		conax1	$⊢ \neg (φ \to ψ) \to \neg ψ$
3	1 2	jcnd	$⊢ \neg (φ \to ψ) \to \neg (((φ \to ψ) \to ψ) \to ψ)$
4	3	con4i	$⊢ (((φ \to ψ) \to ψ) \to ψ) \to (φ \to ψ)$
5		pm2.27	$⊢ (φ \to ψ) \to (((φ \to ψ) \to ψ) \to ψ)$
6	4 5	impbii	$⊢ (((φ \to ψ) \to ψ) \to ψ) \leftrightarrow (φ \to ψ)$