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