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