Theorem xchnxbir

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

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