Theorem nimnbi2

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

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

Proof

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