∀xp(x) given 2. ax q(x) given 3. ex s(x) given 4. ∀x(p(x)∗q(x)∗s(x))→b(x) given 5. ax(p(c) * q(c) * s(c)) -> b(c) 3, existential elimination {x/c} 6. p(c) 1, universal elimination {x/c} 7. q(c) 2, universal elimination {x/c} 8. 6, 7, conjunction 9. 8, 5, conjunction 10. (p(c)∗q(c)∗s(c))→b(c) 4, [choose one] 11. 9,10, modulus ponens 12. 11, existential introduction