Theorem pm4.15

Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)

Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \neg \chi \leftrightarrow \psi \wedge \chi \rightarrow \neg \varphi \)
Proof
l0
con2b
\( \vdash \psi \wedge \chi \rightarrow \neg \varphi \leftrightarrow \varphi \rightarrow \neg (\psi \wedge \chi) \)
nan
\( \vdash \varphi \rightarrow \neg (\psi \wedge \chi) \leftrightarrow \varphi \wedge \psi \rightarrow \neg \chi \)
bitr2i l0 _