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