The axioms, which we have discussed in the previous chapter and have divided into five groups, are not contradictory to one another; that is to say, it is not possible to deduce from these axioms, by any logical process of reasoning, a proposition which is contradictory to any of them. To demonstrate this, it is sufficient to construct a geometry where all of the five groups are fulfilled.
Just formalise this section in ZF, and it drops right out.
Comments
Was it ever proven for A1-4 in ZF?
Presumably: it's not hard. See e.g. https://math.berkeley.edu/~wodzicki/160/Hilbert.pdf §9:
Just formalise this section in ZF, and it drops right out.