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