The OP raises the following question about the implication A ∴ B → A.
I think I am misinterpreting the proof, as it would seem to be implying that under the assumption of B is true, and knowing A is true, then B implies A is true, but this can't be right. Surely B and A can both be true without B entailing A. So how does the proof work?
One way to see what is going on is to consider a truth table. Here is one:
The fourth line in that table shows what happens to the implication when both A and B are true.
Another way is to try to write a proof oneself. Here is one way to do this with a proof checker to make sure the steps are correct:
Here the reiteration (R) rule on line 3 allows us to copy A from line 1 to line 3. One can then rewrite lines 2 and 3 as a conditional using the rule of conditional introduction (→I).
What makes this work is a truth predicate that assigns a true or false value to each of the sentences symbolized as letters. Couple that with inference rules and one has a truth-functional logic. Follow the rules and trust the symbolization can be assigned a truth predicate and the logic flows without considering what it is one is talking about.
Stanford Truth Table Tool: http://web.stanford.edu/class/cs103/tools/truth-table-tool/