This rule can be used forwards to derive the right subformula of an IMPLIES formula from it's left, or backwards on the right sub formula (which is a goal) of an IMPLIES formula to derive the left hand sub formula as a new goal.
To use it forwards:

1. select an empty line and click on Arrow Elimination.
2. then select an IMPLIES formula to be eliminated (the formula must be in the scope of the empty line).
3. then select a formula line that is the same as the left subformula of the IMPLIES formula, which must also be in the empty line's scope.
4. the right subformula of the IMPLIES formula will then be added to your proof.

1. select the goal line which matches the right subformula of the IMPLIES formula you are eliminating and click on Arrow Elimination.
2. then select the IMPLIES formula line you wish to use for the elimination, which must be in the scope of the goal line.
3. the left subformula of the IMPLIES formula will then be added to your proof as a new goal.