Consider the following premises. ~q_2. q_2 <-> q. q_4 <-> p_3. q <-> q_4. p. Can we infer p and ~p_3 from them? If possible, name the inference rules being used at each step.
 From q_2 <-> q, ~q_2 we can infer ~q via biconditional elimination. From q <-> q_4, ~q we can infer ~q_4 via biconditional elimination. From q_4 <-> p_3, ~q_4 we can infer ~p_3 via biconditional elimination. Finally, from p, ~p_3 we can infer p and ~p_3 via conjunction. Therefore, the answer is yes.