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