Theorem xchnxbi

Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014)

	Ref	Expression
Hypotheses	xchnxbi.1	$$⊢\neg \phi \leftrightarrow \psi$$
	xchnxbi.2	$$⊢\phi \leftrightarrow \chi$$
Assertion	xchnxbi	$$⊢\neg \chi \leftrightarrow \psi$$

Proof

Step	Hyp	Ref	Expression
1		xchnxbi.1	$$⊢\neg \phi \leftrightarrow \psi$$
2		xchnxbi.2	$$⊢\phi \leftrightarrow \chi$$
3	2	notbii	$$⊢\neg \phi \leftrightarrow \neg \chi$$
4	3 1	bitr3i	$$⊢\neg \chi \leftrightarrow \psi$$