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