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