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