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