Theorem xchbinx

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

Hypotheses
xchbinx.1
\( \vdash \varphi \leftrightarrow \neg \psi \)
xchbinx.2
\( \vdash \psi \leftrightarrow \chi \)
Conclusion
\( \vdash \varphi \leftrightarrow \neg \chi \)
Proof
l0
xchbinx.1
\( \vdash \varphi \leftrightarrow \neg \psi \)
xchbinx.2
notbii _
\( \vdash \neg \psi \leftrightarrow \neg \chi \)
bitri l0 _