Consider the following premises. p_15 -> p. ~p_23. p_23 <-> p. ~p_15 <-> w_3. Can we infer w_3 from them? If possible, name the inference rules being used at each step.
 From p_23 <-> p we can infer p -> p_23 via biconditional elimination. From p_15 -> p, p -> p_23 we can infer p_15 -> p_23 via transitivity. From p_15 -> p_23, ~p_23 we can infer ~p_15 via modus tollens. From ~p_15 <-> w_3 we can infer ~p_15 -> w_3 via biconditional elimination. Finally, from ~p_15 -> w_3, ~p_15 we can infer w_3 via modus ponens. Therefore, the answer is yes.