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