justification we have term ( id ) and term ( id )

None.

It applies the left multiplicative introduction rule for the conjunction on the formula A ∧ B (in Natural Deduction this corresponds to the elimination rule for the conjunction).

A new sequent with A ∧ B as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses H1 : A and H2 : B are added to the context.