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