Consider the following premises. p -> q_2. s. w -> p. q_2 -> w. q_2 -> ~s. Can we infer w from them? If possible, name the inference rules being used at each step.
 From w -> p, p -> q_2 we can infer w -> q_2 via transitivity. From q_2 -> ~s, s we can infer ~q_2 via modus tollens. From w -> q_2, q_2 -> w we can infer w <-> q_2 via biconditional introduction. Finally, from w <-> q_2, ~q_2 we can infer ~w via biconditional elimination, which contradicts w. Therefore, the answer is no.