Definition: A deduction is in normal form if there is no formula which is a conclusion of an introduction rule and the main premise of the elimination rule of the same connective.
So, in a natural deduction system, one can normalize a proof that contains an introduction rule of a connective followed right after by the elimination rule of the same connective. Here, I have the opposite. First two elimination rules and then the introduction rule of the same connective.
By this definition, the above deduction is in normal form. But still, it can be reduced to a simpler deduction (the trivial A∧B). It seems correct to me, that we can reduce it to just the axiom $A\wedge B$. But how, since the structure of the deduction doesn't have a pair of rules that could be eliminated?
For whoever cannot see the image on the post, I'll give a description of the deduction depicted in it.
(1): $A\wedge B\vdash A$ (by conjunction elimination)
(2): $A\wedge B\vdash B$ (by conjunction elimination, again)
(3): $A, B\vdash A\wedge B$ (by conjunction introduction on (1) and (2))
