Consider the following premises. forall y: W(y). s_4 <-> r_1. W(b) -> r_1. r_1 -> q. Can we infer q from them? If possible, name the inference rules being used at each step.
 From forall y: W(y) we can infer W(b) via universal instantiation. From W(b) we can infer W(b) or s_4 via addition. From s_4 <-> r_1 we can infer s_4 -> r_1 via biconditional elimination. From W(b) -> r_1, s_4 -> r_1, W(b) or s_4 we can infer r_1 via disjunction elimination. Finally, from r_1 -> q, r_1 we can infer q via modus ponens. Therefore, the answer is yes.