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