This rule can only be applied backwards to prove a FOR ALL formula containing an IMPLIES formula, as its sub formula, in one step by declaring a skolem constant and assuming the left hand side of the IMPLIES formula in a box with the right sub formula of the IMPLIES formula as its conclusion.
To use it backwards:

1. select the FOR ALL IMPLIES goal line you wish to use and click on For All Arrow Introduction.
2. a new box will be added to your proof which declares a skolem term and assumes the left subformula of the IMPLIES formula with the right subformula as its conclusion.