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