Theorem impr

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

Hypothesis
impr.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
Proof
impr.1
ex _
imp32 _