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