Theorem xchnxbi

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

Hypotheses
xchnxbi.1
\( \vdash \neg \varphi \leftrightarrow \psi \)
xchnxbi.2
\( \vdash \varphi \leftrightarrow \chi \)
Conclusion
\( \vdash \neg \chi \leftrightarrow \psi \)
Proof
xchnxbi.2
l1
notbii _
\( \vdash \neg \varphi \leftrightarrow \neg \chi \)
xchnxbi.1
\( \vdash \neg \varphi \leftrightarrow \psi \)
bitr3i l1 _