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