We will explain how to state Hindman's theorem in a way that provides a statement provable from ZFC but not from ZF alone. This gives us a way of considering Hindman's theorem as a weak version of the Axiom of Choice; we will discuss where this statement fits within the hierarchy of weak choice principles, and provide a few independence proofs, involving this principle, within ZF ---this will require us to outline the Fraenkel-Mostowski method for providing independence proofs in ZFA.