Theorem jctil

Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)

Hypotheses
jctil.1
\( \vdash \varphi \rightarrow \psi \)
jctil.2
\( \vdash \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \wedge \psi \)
Proof
jctil.2
l1
a1i _
jctil.1
jca l1 _