Consider the following premises. s. q <-> q_12. q. Can we infer s and q_12 from them? If possible, name the inference rules being used at each step.
 From q <-> q_12 we can infer q -> q_12 via biconditional elimination. From q -> q_12, q we can infer q_12 via modus ponens. Finally, from s, q_12 we can infer s and q_12 via conjunction. Therefore, the answer is yes.