Consider the following premises. w -> p_13. w or w_2. p_13 <-> w_2. p_13 -> u_1. Can we infer u_1 from them? If possible, name the inference rules being used at each step.
 From p_13 <-> w_2 we can infer w_2 -> p_13 via biconditional elimination. From w -> p_13, w_2 -> p_13, w or w_2 we can infer p_13 via disjunction elimination. Finally, from p_13 -> u_1, p_13 we can infer u_1 via modus ponens. Therefore, the answer is yes.