Theorem nimnbi2

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

	Ref	Expression
Hypothesis	nimnbi2.1	$$⊢\neg \left(\psi \to \phi \right)$$
Assertion	nimnbi2	$$⊢\neg \left(\phi \leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nimnbi2.1	$$⊢\neg \left(\psi \to \phi \right)$$
2		biimpr	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\psi \to \phi \right)$$
3	1 2	mto	$$⊢\neg \left(\phi \leftrightarrow \psi \right)$$