We give an irredundant axiomatization of the complete ordered field of real numbers. In particular, we show that all the field axioms for multiplication with the exception of the distributive property may be deduced as "theorems" in our system. We also provide a complete proof that the axioms we have chosen are independent.