Consider the following premises. r. r -> w. w <-> q. Can we infer ~w from them? If possible, name the inference rules being used at each step.
 From r we can infer r or q via addition. From w <-> q we can infer q -> w via biconditional elimination. Finally, from r -> w, q -> w, r or q we can infer w via disjunction elimination, which contradicts ~w. Therefore, the answer is no.