Proposition Logic problem

Anyone good with proposition logics? that can help out?
im stuck on one question and can't figure out the next step.

The question states : Use the rules of inference to prove the following.
(p -> q) ^ (r -> s) ^ [t -> ~(q V s) ^ t => (~p ^ ~r)
note : the " ~ " sign means NOT,
the " ^ " sign means AND,
the " -> " sign means implies/conditional
the " V " sign means OR
the " => " sign means resultant or conclusion is.

I've set up my working up to look like this.
P -> q H1(Hypothesis 1)
r -> s H2(Hypothesis 2)
t -> ~(q V s) H3(Hypothesis 3)
t H4(Hypothesis 4)
_____________
~p ^ ~r C (Conclusion)

Step one. I got H4 with H3 and AND both of them >> H4 ^ H3 which gives:

t ^ [t -> ~(q V s)] and since t ^ t cancels out with the modus ponens rules it leaves us with ~(q V s).

So now that H4 and H3 is gone we have H1 and H2 left. This is where i got stuck.

I decided to use de morgan's law to simplify which gave me >> ~(q V s) => ~q ^ ~s and we can call this theory one (1).

So far i've only got up to this part and now i'm stuck could you help me figured out what i need to do next?

Working : t ^ [t -> ~(q V s)] <=> ~(q V s) H4 ^ H3
<=> ~q ^ ~s (1).

Next step = ? please help

Your next step would be to use the Law of Contrapositives to change p -> q and r -> s into ~q -> ~p and ~s -> ~r.

Since you know ~q ^ ~s already, you're a short step away from your goal.
Nicely done so far!

oh ok thnx alot let me try out the next step.

Damn... i suck bad...

is (~p -> ~q) ^ (~q ^ ~s) possible? using the Hypothecial Syllogism concept. i know it works for if both of them are conditional but just wondering if this method works?

if it does would it look something like ~p->~s or ~p^~s ._.

if ~p->~s works out then... it would be alot easier because then i would just use Hypothetical syllgism law again for ~p->~s ^ ~s->~r which gives me ~p->~r but... then again it doesnt work out... sorry im really bad with this topic. a little more help please?

opps sorry its suppose to be ~q -> ~p not ~p -> ~q my bad.

so that would mean :

(~q -> ~p) ^ (~q ^ ~s) using exportation... is it possible?
gives (~p ^ ~s) -> ~q ? ._. i don't know sorry =/

Ok i think i got it but could someone check the answer for me? if i'm wrong let me know where i got wrong.

t ^ [t -> ~(q V s)] <=> ~(q V s) ... H4 ^ H3 Modus ponens
<=> ~q ^ ~s (1) ... de morgan's law

p -> q => ~q -> ~p (2) ... Contrapositive
r -> s => ~s -> ~r (3) ... Contrapositive

(~q -> ~p) ^ (~q ^ ~s) .... (2) ^ (1)
=> ~p ^ ~s ... Disjunuctive Syllogism
=> ~s ^ ~p (4) ... Commutativity

(~s -> ~r) ^ (~s ^ ~p) (3) ^ (4)
=> ~r ^ ~p ... Disjunctive Syllogism
=> ~p ^ ~r ... Commutativity <--- Conclusion

opps i think i have the laws wrong... but could someone please check my answer? and let me know if i got it right or wrong... if wrong please show me where i went wrong.