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