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