In Terence Tao's Analysis, he states
The axiom is almost universally accepted by mathematicians. One reason for this confidence is a theorem due to the great logician Kurt Godel, who showed that a result proven using the axiom of choice will never contradict a result proven without the axiom of choice. More precisely, Godel demonstrated that the axiom of choice is undecidable; it can neither be proved nor disproved from the other axioms of set theory, so long as those axioms are themselves consistent.
Then he writes
In practice, this means that any “real-life” application of analysis (more precisely, any application involving only “decidable” questions) which can be rigorously supported using the axiom of choice, can also be rigorously supported without the axiom of choice, though in many cases it would take a much more complicated and lengthier argument to do so if one were not allowed to use the axiom of choice. Thus one can view the axiom of choice as a convenient and safe labour-saving device in analysis.
In ZF, if a proposition is "decidable", and if we prove the proposition in ZFC, then it is true in ZF. I understand it. If we prove sth is true in ZFC, then it is undecidable or true in ZF. but I think the hardest part is to demonstrate a proposition is "decidable". How can we do that? Is there anyway to prove a proposition "decidable"? So I think the axiom of choice is not safe. I don't understand Tao's words. Also, I don't understand why he asserts "real-life" application is always "decidable".