Consider the following premises. forall x: S(x) <-> P(x). forall x: S(x) -> P(x). Can we infer S(c) -> P(c) from them?
 From forall x: S(x) <-> P(x) we can infer forall x: P(x) -> S(x). From forall x: P(x) -> S(x), forall x: S(x) -> P(x) we can infer forall x: P(x) <-> S(x). From forall x: P(x) <-> S(x) we can infer P(c) <-> S(c). Finally, from P(c) <-> S(c) we can infer S(c) -> P(c). Therefore, the answer is yes.