Theorem notbid

Description: Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994)

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

Proof

Step	Hyp	Ref	Expression
1		notbid.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
2		notnotb	$$⊢\psi \leftrightarrow \neg \neg \psi$$
3		notnotb	$$⊢\chi \leftrightarrow \neg \neg \chi$$
4	1 2 3	3bitr3g	$$⊢\phi \to \left(\neg \neg \psi \leftrightarrow \neg \neg \chi \right)$$
5	4	con4bid	$$⊢\phi \to \left(\neg \psi \leftrightarrow \neg \chi \right)$$