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