Consider the following premises. p <-> s. w_4 or s. ~w_4. Can we infer p from them? If possible, name the inference rules being used at each step.
 From w_4 or s, ~w_4 we can infer s via disjunctive syllogism. From p <-> s we can infer s -> p via biconditional elimination. Finally, from s -> p, s we can infer p via modus ponens. Therefore, the answer is yes.