This rule can only be used backwards on a goal IMPLIES line to create a box (subproof), with the left hand side of IMPLIES formula as an assumption and it's right hand side as a conclusion.
To use this rule backwards:
select the goal line, which must be an IMPLIES formula, and click on Arrow Introduction.
this will add a new box to your proof with the left hand side of the goal line as its assumption and the IMPLIES formula's right hand side as its conclusion.
