Consider the following premises. forall x_13: P_13(x_13) -> Q_13(x_13). p_2 or ~Q_13(j). forall x_13: Q_13(x_13) -> P_13(x_13). Can we infer P_13(j) -> p_2 from them?
 From forall x_13: P_13(x_13) -> Q_13(x_13), forall x_13: Q_13(x_13) -> P_13(x_13) we can infer forall x_13: P_13(x_13) <-> Q_13(x_13). From forall x_13: P_13(x_13) <-> Q_13(x_13) we can infer P_13(j) <-> Q_13(j). From p_2 or ~Q_13(j) we can infer Q_13(j) -> p_2. From P_13(j) <-> Q_13(j) we can infer P_13(j) -> Q_13(j). Finally, from P_13(j) -> Q_13(j), Q_13(j) -> p_2 we can infer P_13(j) -> p_2. Therefore, the answer is yes.