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