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