This rule can be used forwards to derive a subformula from an AND formula, or backwards to derive a new goal which is a conjunction of the current goal and some other formula.
To use it forwards:

1. select an empty line and click on And Elimination.
2. then select the AND formula line you wish to apply the rule to (this line must be in the scope of the empty line).
3. when prompted, enter the side of the AND formula you want to derive (by entering "l" for left or "r" for right) in the input window.
4. the subformula you specified will then appear as a new line in your proof.

1. select a goal line and click on And Elimination.
2. you will be prompted to choose whether the current goal should go on the left "l" or right "r" or the new goal (And formula).
3. you will then be prompted to type in the formula to appear on the other side of the conjunction.