Injecting premises into two implicational premises connected by a tensor (multiplicative conjunction) in linear logic I have another question regarding linear logic: I want to get to the proof E, using the premises in (1-4). Is this at all possible?
1: $A$
2: $C$
3: $(A\multimap B)\otimes(C\multimap D)$
4: $B\multimap (D\multimap E)$
I originally hoped that I could simply reverse the tensor in (3) (making $(A\multimap B)$ and $(C\multimap D)$ individual premises), so I could inject the premises from (1) and (2). If that had been possible, I could have used assumed premises for (4) in order to use the conjunction elimination rule (which essentially states that I could replace the assumed $B$ and $D$ with $(B\otimes D)$ to derive E. Since I was told that this impossible, however, I am looking for another way to get to E, using the premises described above.
I hope that this question is less vague than my last one. If it is not, I apologise. I cannot see how I can make my question any clearer with my current level of knowledge in logic (or mathematical formalism).
I'm neither a logican nor mathematician; I'm currently looking into glue semantics, which uses Linear Logic to derive the meaning of a sentence. So I am grateful for any and all assistance.
 A: Well, this is very easy, but because linear logic might be considered a little too specialized for Mathematics StackExchange, I'll answer. 
Since the natural semantics of MLL (multiplicative linear logic) is in $\ast$-autonomous categories, which are special symmetric monoidal closed categories, it will suffice to construct a morphism 
$$A \otimes C \otimes [(A \multimap B) \otimes (C \multimap D)] \otimes (B \multimap (D \multimap E)) \to E \qquad (1)$$ 
using the language of smc categories. Using evaluation maps $A \otimes (A \multimap B) \to B$ and $C \otimes (C \multimap D) \to D$ together with associativity and symmetry isomorphisms, we easily get a morphism 
$$A \otimes C \otimes [(A \multimap B) \otimes (C \multimap D)] \otimes (B \multimap (D \multimap E)) \to B \otimes D \otimes (B \multimap (D \multimap E)) \qquad (2)$$ 
and using similarly an evaluation $B \otimes (B \multimap (D \multimap E)) \to D \multimap E$ plus associativities, symmetries, we arrive at a morphism 
$$B \otimes D \otimes (B \multimap (D \multimap E)) \to D \otimes (D \multimap E) \qquad (3)$$ 
and we compose $(2)$ and $(3)$ with an evaluation map $D \otimes (D \multimap E) \to E$ to get an arrow of type $(1)$. 
I haven't seen your other question; I'll have a look. 
