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