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
¬,∧,∨,→,↔