Consider the following premises. ~p_1. p_1 <-> w. t_4 or w. Can we infer t_4 from them? If possible, name the inference rules being used at each step.
 From p_1 <-> w, ~p_1 we can infer ~w via biconditional elimination. From t_4 or w we can infer ~w -> t_4 via rewriting. Finally, from ~w -> t_4, ~w we can infer t_4 via modus ponens. Therefore, the answer is yes.