Consider the following premises. forall z: T(z) -> Q(z). forall z: Q(z) <-> T(z). ~Q(f_4). Can we infer ~T(f_4) from them?
 From forall z: Q(z) <-> T(z) we can infer forall z: Q(z) -> T(z). From forall z: Q(z) -> T(z), forall z: T(z) -> Q(z) we can infer forall z: Q(z) <-> T(z). From forall z: Q(z) <-> T(z) we can infer Q(f_4) <-> T(f_4). From Q(f_4) <-> T(f_4) we can infer T(f_4) -> Q(f_4). Finally, from T(f_4) -> Q(f_4), ~Q(f_4) we can infer ~T(f_4). Therefore, the answer is yes.