Consider the following premises. forall y: W_4(y) -> T_4(y). q_4 -> W_4(f). T_4(f) -> q_4. Can we infer q_4 <-> W_4(f) from them? If possible, name the inference rules being used at each step.
 From forall y: W_4(y) -> T_4(y) we can infer W_4(f) -> T_4(f) via universal instantiation. From W_4(f) -> T_4(f), T_4(f) -> q_4 we can infer W_4(f) -> q_4 via transitivity. Finally, from q_4 -> W_4(f), W_4(f) -> q_4 we can infer q_4 <-> W_4(f) via biconditional introduction. Therefore, the answer is yes.