Jon Sterling on Nostr: You started off right. Your goal was an implication, so you applied the introduction ...

You started off right. Your goal was an implication, so you applied the introduction rule.

Then your goal was (A => B) |- ((B => C) => (A => C)).

That's another implication, so you might as well apply the introduction rule again.

Now you would have:

(A => B), (B => C) |- A => C

Here you have another implication, so you might as well apply the intro rule once more. Then you'd have:

(A => B), (B => C), A |- C

Now you can start working your way downward with elim rules.