Theorem nimnbi

Description: If an implication is false, the biconditional is false. (Contributed by Glauco Siliprandi, 15-Feb-2025)

	Ref	Expression
Hypothesis	nimnbi.1	⊢ ¬ ( 𝜑 → 𝜓 )
Assertion	nimnbi	⊢ ¬ ( 𝜑 ↔ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nimnbi.1	⊢ ¬ ( 𝜑 → 𝜓 )
2		biimp	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜑 → 𝜓 ) )
3	1 2	mto	⊢ ¬ ( 𝜑 ↔ 𝜓 )