Theorem jccil

Inference conjoining a consequent of a consequent to the left of the consequent in an implication. Remark: One can also prove this theorem using syl and jca (as done in jccir ), which would be 4 bytes shorter, but one step longer than the current proof. (Proof modification is discouraged.) (Contributed by AV, 20-Aug-2019.)

Hypotheses
jccir.1
\( \vdash \varphi \rightarrow \psi \)
jccir.2
\( \vdash \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \wedge \psi \)
Proof
l0
jccir.1
jccir.2
jccir l0 _
ancomd _