Theorem pm4.14

Theorem *4.14 of [WhiteheadRussell] p. 117. Related to con34b. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Oct-2012.)

Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \leftrightarrow \varphi \wedge \neg \chi \rightarrow \neg \psi \)
Proof
con34b
l1
imbi2i _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \leftrightarrow \varphi \rightarrow \neg \chi \rightarrow \neg \psi \)
l2
impexp
\( \vdash \varphi \wedge \psi \rightarrow \chi \leftrightarrow \varphi \rightarrow \psi \rightarrow \chi \)
impexp
\( \vdash \varphi \wedge \neg \chi \rightarrow \neg \psi \leftrightarrow \varphi \rightarrow \neg \chi \rightarrow \neg \psi \)
3bitr4i l1 l2 _