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

Metamath Proof Explorer

Theorem notbii

Description: Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993) (Proof shortened by Wolf Lammen, 19-May-2013)

		Ref	Expression
	Hypothesis	notbii.1	$⊢ φ \leftrightarrow ψ$
	Assertion	notbii	$⊢ \neg φ \leftrightarrow \neg ψ$

Step	Hyp	Ref	Expression
1		notbii.1	$⊢ φ \leftrightarrow ψ$
2		notbi	$⊢ (φ \leftrightarrow ψ) \leftrightarrow (\neg φ \leftrightarrow \neg ψ)$
3	1 2	mpbi	$⊢ \neg φ \leftrightarrow \neg ψ$