Jon Sterling on Nostr: nprofile1q…4rs4v You started off right. Your goal was an implication, so you ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpq0p4hclaqjlup0fwjt5ke3mgxq6rtjth8u62yfv0s62xkxp04wjaqa4rs4v (nprofile…rs4v) 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.