T5.6 4 of 6

OK, then, our derivation can be done quite simply if we can only do the right pattern matching:

If you think about HS as a way to prove your ultimate goal 'F>H'. This makes you think about a preliminary goal (here 'G>H') that will suggest IM.  Seeing the problem in this way, doing the goal analysis to the point of having preliminary goals based on seeing the right patterns, takes time. But with a little practice, it saves lots of time.

However, if you don't see the patterns fairly quickly, just assume the opposite of your ultimate goal and go through the longer proof by RD: