The implyR proof rule proves an implication P→Q
by assuming its left-hand side P
(by pushing it into the assumptions in the antecedent) and proving its right-hand side Q
.
This exploits that the meaning of a sequent is implicational: (the conjunction of its) left-hand side implies (the disjunction of) its right-hand side.
See also
¬,∧,∨,→,↔