WORKING THROUGH A DIRECT DERIVATION

With a direct derivation we need to think backwards from the intended conclusion to what we have in the premises.

Let's say we have the following argument form:  (P v Q) -> R,  P v S, ~(S v T)  |- R

We see R in the first premise, but in order to get R we need to know P v Q as true.  Now let's think about our "magic" rule of addition, which would let us go either from P or Q to P v Q.   We see P itself in the second premise, but we would need to eliminate the wedge to do this, and so we need to know ~S.  If we look at the third premise we see that we can use our DM equivalence rule to turn it into ~S & ~T, then use simplification to eliminate the ampersand.

Putting this all together, we can then develop our proof, beginning with what we saw last in our analysis.
1.  (P v Q -> R
2.  P v S
3.  ~(S v T)     / show R
4.  ~S & ~T    3,  DM
5.  ~S            4,  Simp
6.  P              2,5,  DS
7.  P v Q        6,  Add
8.  R              1,7  MP


In applying our inference rules, a crucial point to remember is that they apply only to the main connective in an expression.  They cannot be used inside a parenthesis, as would happen with an equivalence rule (Implication, for instance).  Be careful to remember that the rules for the most part are involved with either eliminating or introducting a connective (including a quantifier).

P & Q  |-  P     Simplification  (Simp)    eliminates the ampersand        
P, Q  |-  P & Q      Conjunction  (Conj)   introduces the ampersand
P v Q, ~P  |- Q      Disjunctive syllogism  (DS)   eliminates the wedge
P  |- P v Q     Addition  (Add)   introduces the wedge
P -> Q, P |- Q       Modus ponens  (MP)   eliminates the arrow when we know the antecedent is true
P -> Q, ~Q  |- ~P      Modus tollens  (MT)   eliminates the arrow when we know the consequent is false
P -> Q, Q -> R |- P -> R     Hypothetical syllogism  (HS)  
(x)Fx  |-  Fa     Universal instantiation  (UI)   eliminates a universal quantifier
Fa  |- (x)Fa      Universal generalization  (UG)   introduces a universal quantifier
normally this requires that the name in question cames from a previous application of the UI rule; the exception is when in a conditional proof we establish a statement such as Fa -> Ga  and then go to (x)(Fx - Gx) 
(Ex)Fx  |- Fa    Existential instantiation  (EI)    eliminates an existential quantifier
the name brought into play must be new--not appearing either in the statement of the argument fom or in a previous step
Fa |- (Ex)Fx     Existential generalization  (EG)   introduces an existential quantiifer

Let's look at an argument that involves the use of quantifiers.

(x)[(Ax v Bx) -> Cx], (Ex)Ax v (Ex)Dx, ~(Ey)(Dy v Ey)  |- (Ez)Cz

What I've done here is follow the same basic pattern that we had in the first example, except we need to work correctly with our quantifiers.  In particular, note that in the first premise the main connective is itself a quantifier while in the second it is the wedge.  As we go through, compare the steps with what we have above.
1.  (x)[(Ax v Bx)) -> Cx]
2.  (Ex)Ax v (Ex)Dx
3.  ~(Ey)(Dy v Ey)         / show (Ez)Cz
4.  (y)~(Dy v Ey)            3,  QN
5.  (y)(~Dy & ~Ey)         4,  DM
6.  ~Da & ~Ea               5,  UI
7.  ~Da                         6,  Simp
8.  (x)~Dx                      7,  UG
9.  ~(Ex)Dx                   8,  QN
10.  (Ex)Ax                    2,9,  DS
11.  Ab                          10,  EI        watch how we needed to apply the new name rule with an existential quantifier
12.  (Ab v Bb) -> Cb        1,  UI
13.  Ab v Bb                   11,  Add
14.  Cb                           12,13,  MP
15.  (Ez)Cz                     14,  EG

This is a more complicated proof, because we needed to eliminate and then reintroduce quantifiers as we went along.   One mistake to avoid would be trying to instantiate the second premise right off.  The wedge is the main connective, so that needs to be taken care of first.  The process involves an interesting step worth noting for the future. Also, in this proof, note that we are free to switch from one variable (x or y or z) to another as long as we go through the appropriate steps to eliminate one and then generalize with the other.