The implyL proof rule uses an implication P→Q among its assumptions by first proving its left-hand side P and then, on a separate branch, assuming its right-hand side Q, which, according to the assumption P→Q, follows from P.

See also