Consider the following premises. t <-> q. ~r_3. q -> r_3. Can we infer t from them? If possible, name the inference rules being used at each step.
 From q -> r_3, ~r_3 we can infer ~q via modus tollens. Finally, from t <-> q, ~q we can infer ~t via biconditional elimination, which contradicts t. Therefore, the answer is no.