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