Consider the following premises. p_4 <-> W(a). forall z_1: T_3(z_1) -> W(z_1). forall z_1: ~T_3(z_1). forall z_1: W(z_1) -> T_3(z_1). Can we infer ~p_4 from them? If possible, name the inference rules being used at each step.
 From forall z_1: W(z_1) -> T_3(z_1), forall z_1: T_3(z_1) -> W(z_1) we can infer forall z_1: W(z_1) <-> T_3(z_1) via universal biconditional introduction. From forall z_1: W(z_1) <-> T_3(z_1), forall z_1: ~T_3(z_1) we can infer forall z_1: ~W(z_1) via universal biconditional elimination. From forall z_1: ~W(z_1) we can infer ~W(a) via universal instantiation. Finally, from p_4 <-> W(a), ~W(a) we can infer ~p_4 via biconditional elimination. Therefore, the answer is yes.