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