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