Theorem expl

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

Hypothesis
expl.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \theta \)
Proof
expl.1
exp31 _
impd _