Some of the other *answers* seem to be based on the assumption that in ordinary mathematics, one needs (at least) two separate consequences of the full AC: (1) dependent choice (ADC); and (2) existence of nonprincipal ultrafilters.

As is well known, avoidance of choice as much as possible is motivated by its unintuitive consequences, as detailed [here](https://mathoverflow.net/questions/20882/most-unintuitive-application-of-the-axiom-of-choice).  In this context, some of our [recent work](https://doi.org/10.1016/j.apal.2021.102959) suggests that ingredient (2) above may be reducible to (1).  Namely, we constructed a conservative extension of ZF+ADC where infinitesimals are found within $\mathbb R$, eschewing any need for nonprincipal ultrafilters (in the sense of conservativity just mentioned).  We showed, for example, that the Lebesgue measure admits an infinitesimal construction (via counting measures), and that Peano existence theorem similarly admits an intuitive infinitesimal proof.  

It would be interesting to explore other areas of mathematics where ultrafilters are used, to determine whether analogous conservative extensions can be constructed that would enable one to bypass the dependence on the existence of ultrafilters.

The moral one draws from this is that the two goals of the revolution of 1870: (a) elimination of infinitesimals, and (b) increased rigor via formalisation of foundations, are actually *entirely unrelated*, contrary to much flak in the historical literature.  To put it another way, the reason it is so hard to put infinitesimals back into mathematics is because there were taken out to begin with when the foundations were formalized.  Notably, one shortcoming of ZF was its failure to formalize the Leibnizian distinction between assignable and inassignable quantities, which had been the source of infinitesimals in analysis for centuries before they were eliminated from the foundations.