Theorem pm5.75

Theorem *5.75 of [WhiteheadRussell] p. 126. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2012.) (Proof shortened by Kyle Wyonch, 12-Feb-2021.)

Conclusion
\( \vdash (\chi \rightarrow \neg \psi) \wedge (\varphi \leftrightarrow \psi \vee \chi) \rightarrow (\varphi \wedge \neg \psi \leftrightarrow \chi) \)
Proof
l0
anbi1
\( \vdash (\varphi \leftrightarrow \psi \vee \chi) \rightarrow (\varphi \wedge \neg \psi \leftrightarrow (\psi \vee \chi) \wedge \neg \psi) \)
biorf
bicomd _
pm5.32ri _
\( \vdash (\psi \vee \chi) \wedge \neg \psi \leftrightarrow \chi \wedge \neg \psi \)
l4
bitrdi l0 _
\( \vdash (\varphi \leftrightarrow \psi \vee \chi) \rightarrow (\varphi \wedge \neg \psi \leftrightarrow \chi \wedge \neg \psi) \)
abai
rbaib _
\( \vdash (\chi \rightarrow \neg \psi) \rightarrow (\chi \wedge \neg \psi \leftrightarrow \chi) \)
sylan9bbr l4 _