Theorem jctild

Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses
jctild.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
jctild.2
\( \vdash \varphi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \wedge \chi \)
Proof
jctild.2
l1
a1d _
jctild.1
jcad l1 _