Consider the following premises. u or ~r. r_1 -> r. u -> r_1. Can we infer r <-> r_1 from them? If possible, name the inference rules being used at each step.
 From u or ~r we can infer r -> u via rewriting. From r -> u, u -> r_1 we can infer r -> r_1 via transitivity. Finally, from r -> r_1, r_1 -> r we can infer r <-> r_1 via biconditional introduction. Therefore, the answer is yes.