Theorem expr

Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis
expr.1
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \chi \rightarrow \theta \)
Proof
expr.1
exp32 _
imp _