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