Theorem pm4.87

Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Eric Schmidt, 26-Oct-2006.)

Conclusion
\( \vdash (\varphi \wedge \psi \rightarrow \chi \leftrightarrow \varphi \rightarrow \psi \rightarrow \chi) \wedge (\varphi \rightarrow \psi \rightarrow \chi \leftrightarrow \psi \rightarrow \varphi \rightarrow \chi) \wedge (\psi \rightarrow \varphi \rightarrow \chi \leftrightarrow \psi \wedge \varphi \rightarrow \chi) \)
Proof
l0
impexp
bi2.04
l2
pm3.2i l0 _
impexp
bicomi _
pm3.2i l2 _