Theorem xchbinxr

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

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