Theorem pm5.71

Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.)

Conclusion
\( \vdash (\psi \rightarrow \neg \chi) \rightarrow ((\varphi \vee \psi) \wedge \chi \leftrightarrow \varphi \wedge \chi) \)
Proof
l0
orel2
orc
impbid1 l0 _
l3
anbi1d _
pm2.21
pm5.32rd _
ja l3 _