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