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