This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (ψ \to φ)$
	Assertion	nimnbi2	$⊢ \neg (φ \leftrightarrow ψ)$

Step	Hyp	Ref	Expression
1		nimnbi2.1	$⊢ \neg (ψ \to φ)$
2		biimpr	$⊢ (φ \leftrightarrow ψ) \to (ψ \to φ)$
3	1 2	mto	$⊢ \neg (φ \leftrightarrow ψ)$