Consider the following premises. ~u_3. r or u. u_3 <-> p. ~r. Can we infer u and ~p from them? If possible, name the inference rules being used at each step.
 From u_3 <-> p we can infer p -> u_3 via biconditional elimination. From r or u, ~r we can infer u via disjunctive syllogism. From p -> u_3, ~u_3 we can infer ~p via modus tollens. Finally, from u, ~p we can infer u and ~p via conjunction. Therefore, the answer is yes.