Slide 1: Since our goal is an existentially quantified sentence, as is one of our premises, it looks like we'll be using existential elimination, so we might as well go ahead and assume a substitution instance.

Slide 2: We know that we'll have to use existential introduction in order to derive our goal, which tells us that we will need a substituion instance of that goal as our new subgoal.

Slide 3: Since our new subgoal is a conjunction, we can work backwards from it to the individual conjuncts.

Slide 4: Our left-hand conjunct can immediately be extracted from our assumption...

Slide 5: ...but the right-hand conjunct will require more effort.

Slide 6: Obviously we need to use negation introduction for our newest subgoal, so we begin the required subderivation.

Slide 7: Now all we need is a contradiction. The identity claim we have just assumed makes it possible to derive that contradiction, we just need to lay the groundwork first.

Slide 8: The only thing left to do is to apply identity elimination, deriving our required contradiction and thus completing the derivation.

Slide 9: (no voice over)