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