Metamath Proof Explorer

Theorem dfbi1ALTb

Description: Further shorten dfbi1ALTa using simprimi . (Contributed by Eric Schmidt, 22-Oct-2025) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-bi	$⊢ \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))$
2		df-bi	$⊢ \neg ((((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ)))) \to \neg (\neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))))$
3	2	simprimi	$⊢ \neg (((φ \leftrightarrow ψ) \to \neg ((φ \to ψ) \to \neg (ψ \to φ))) \to \neg (\neg ((φ \to ψ) \to \neg (ψ \to φ)) \to (φ \leftrightarrow ψ))) \to ((φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ)))$
4	1 3	ax-mp	$⊢ (φ \leftrightarrow ψ) \leftrightarrow \neg ((φ \to ψ) \to \neg (ψ \to φ))$