> I think we can simplify that slightly @Matthew
>
> We have your (A) and (B), ie \$$x\otimes (x\multimap y) \leq y\$$ and \$$y \otimes (y\multimap z) \leq z\$$.

Sure, but it's important to note that we are using commutativity to flip (B).

> Therefore \$$x\otimes (x\multimap y) \otimes (y\multimap z) \leq y \otimes (y\multimap z) \leq z\$$.
>
> So by adjunction \$$(x\multimap y) \otimes (y\multimap z) \leq (x\multimap z)\$$.

Again, you are using commutativity...

That's pedantry, I know. The proof is ugly and long if we don't just use commutativity implicitly.

However, I am not sure if this theorem is true in a closed non-commutative monoidal preorder.