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

Metamath Proof Explorer

Theorem bibif

Description: Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007) (Proof shortened by Wolf Lammen, 28-Jan-2013)

		Ref	Expression
	Assertion	bibif	$⊢ \neg ψ \to ((φ \leftrightarrow ψ) \leftrightarrow \neg φ)$

Step	Hyp	Ref	Expression
1		nbn2	$⊢ \neg ψ \to (\neg φ \leftrightarrow (ψ \leftrightarrow φ))$
2		bicom	$⊢ (ψ \leftrightarrow φ) \leftrightarrow (φ \leftrightarrow ψ)$
3	1 2	bitr2di	$⊢ \neg ψ \to ((φ \leftrightarrow ψ) \leftrightarrow \neg φ)$