Consider the following premises. p_11 <-> s_3. p_11 -> ~p_3. p_3. Can we infer ~s_3 or q_3 from them? If possible, name the inference rules being used at each step.
 From p_11 -> ~p_3, p_3 we can infer ~p_11 via modus tollens. From p_11 <-> s_3, ~p_11 we can infer ~s_3 via biconditional elimination. Finally, from ~s_3 we can infer ~s_3 or q_3 via addition. Therefore, the answer is yes.