Consider the following premises. w -> p. p -> w. ~t_4. p -> w. p <-> t_4. Can we infer ~w from them? If possible, name the inference rules being used at each step.
 From p -> w, w -> p we can infer p <-> w via biconditional introduction. From p <-> w we can infer w -> p via biconditional elimination. From p <-> t_4, ~t_4 we can infer ~p via biconditional elimination. From w -> p, p -> w we can infer w <-> p via biconditional introduction. Finally, from w <-> p, ~p we can infer ~w via biconditional elimination. Therefore, the answer is yes.