Consider the following premises. forall z_4: Q(z_4) or P(z_4). p_1 <-> P(b). ~Q(b). Can we infer p_1 from them? If possible, name the inference rules being used at each step.
 From forall z_4: Q(z_4) or P(z_4) we can infer Q(b) or P(b) via universal instantiation. From Q(b) or P(b), ~Q(b) we can infer P(b) via disjunctive syllogism. From p_1 <-> P(b) we can infer P(b) -> p_1 via biconditional elimination. Finally, from P(b) -> p_1, P(b) we can infer p_1 via modus ponens. Therefore, the answer is yes.