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