Avatrin said:
The only steps here I understand are 1 to 5. I don't know why 6 and 7 are true.
Line 2 makes an assumption, and thereby opens what is called a conditional proof (CP). The conditional proof is closed by
discharging the assumption that made it, at a later line. We'll come to what that means shortly.
Conditional proofs can be nested within each other. Above there are two CPs, one commencing at 2 and ending at 7, the other commencing at 3 and ending at 6. The last line of a CP closes the proof by asserting A->B, where A was the assumption that opened the proof and B is the statement immediately before the closing line. Closing the proof 'discharges' the assumption A, which means that A is no longer assumed but, in its place, we have A->B, which is valid everywhere from there on within the next enclosing CP.
All interim results deduced inside a CP are invalid outside it, except for the closing statement.
So line 6 closes the inner CP giving the result (3)->(5)
Then line 7 closes the outer CP giving the result (2)->(6)
The first example is actually written in a confusing manner. A better way to write it is:
(1) Given: b
(2) Suppose: a
(3) b (from 1)
(4) By implication with (3) and (1), a→b
Written that way, we see that a CP is opened at (2) and closed at (4) with the statement (2)->(3).
It's possible to loosen the rules for closing CPs so that the antecedent of the closing statement (the statement after the arrow ->) can be any statement that is in scope at that point. That is the approach that was taken in the first example. But that requires explicitly laying out the scoping rules, which may be more complex than you want to get.