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