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