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