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