[FOM] reflection principle for inaccessible

[Paul Blain Levy]

Hi,

Let phi be a sentence (no free variables) such that ZFC proves "For
every strongly inaccessible kappa, phi relativized to kappa".

Does it follow that ZFC proves "If a strong inaccessible exists, then phi"?

My guess would be that there's a counterexample along the lines of "For
every x, the system ZFC(x) is consistent", where ZFC(x) is a version of
ZFC that incorporates x as a primitive, but I know of no such construction.

Paul