Theorem nimnbi

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

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

Proof

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