Consider the following premises. s_1 -> P_15(c). Q_15(c) -> s_1. forall x_15: P_15(x_15) <-> Q_15(x_15). Can we infer s_1 -> Q_15(c) from them? If possible, name the inference rules being used at each step.
 From forall x_15: P_15(x_15) <-> Q_15(x_15) we can infer forall x_15: P_15(x_15) -> Q_15(x_15) via universal biconditional elimination. From forall x_15: P_15(x_15) -> Q_15(x_15) we can infer P_15(c) -> Q_15(c) via universal instantiation. Finally, from s_1 -> P_15(c), P_15(c) -> Q_15(c) we can infer s_1 -> Q_15(c) via transitivity. Therefore, the answer is yes.