@Protoman2050,
You could do your proof in any numbers of ways. But this may be the shortest and the simplest way with these inference and replacement rules. This usually turns out to reveal the
essential arguments of an argument and reveal unnecessary assumptions you may have had. Simply, you may have excess premises on the block that need to be cut away to reveal a more stream lined argument..
For the way the proof was done, we see that the double negation is really redundant because ~~D = D, we just used a semantic twist to get that for the purpose of our proof. Also, since we are trying to streamline your argument, the communication can be corrected by redoing your first premise. Successfully doing these changes cut back your argument by 2 premises and still have the same effect.
So the word play with ~~D (i.e. it is not not Delta) and the disjunction are not really needed. The syntax of your literal argument (the unknown variable) can be mended.
Keep in mind I'm saying this because you placed emphasis on a literal translation. In a regular proof, you do not need to worry about this.
