Propositional logic and first-order logic are theories in ZFC. The principle of structural induction is a theorem of ZFC. Is that what justifies the usage of structural induction in propositional logic and first-order logic?
By justifying I really mean proving, that is, tracing back to axioms.
Meaning of structural induction: Sturctural induction.
This is sort-of true, with a caveat. I would put it like this: the principle is a theorem of ZFC, so that is one way to justify its use in proving theorems about proposition calculus, likewise predicate calculus.
As the Wikipedia article mentions, structural induction is a special case of a general result about well-founded partial orders. The formulas of proposition logic form a well-founded partial order under the "is a subformula of" relation. Likewise for predicate calculus (aka first-order logic).
So as applied to the predicate calculus, this would be a proof that first shows something is true for atomic formulas, then shows that if it is true for $\alpha$, $\beta$, and $\gamma(x)$, then it is true for $\neg\alpha$, $\alpha\wedge\beta$, and $\exists x\gamma(x)$. And then concludes from this that it holds for all formulas. Similarly with the propositional calculus. Here the base case is propositional variables, and you still have the connectives, but you don't have to worry about quantifiers or terms.
Note that I am talking about proving results about the propositional (or predicate) calculus. For example, showing that every formula of propositional logic has an equivalent in disjunctive normal form, or that every formula of first-order logic has an equivalent in prenex normal form. Or a particularly simple example you mentioned: that every formula has equal numbers of left and right parentheses.
In contrast, a proof in one of these calculi is a different beast. As an example, consider this proof of the formula $A\to A$, in two versions of the propositional calculus. You'll see that no axioms of ZFC appear. Indeed, it's impossible even to express the axioms of ZFC in the propositional calculus: quantifiers and the relation symbol $\in$ are essential.
This "about vs. in" distinction is an example of metamathematics vs. mathematics. A formal system, like the predicate calculus, consists (from one viewpoint) just of strings of symbols with rules for manipulating them. We can apply ordinary mathematical reasoning to this "symbol manipulation game". But the predicate calculus itself is formalized reasoning. So we have two layers, the so-called mathematical layer (namely proofs in the calculus), and the metamathematical layer (proofs about the predicate calculus). And likewise for the propositional calculus.
What sort of reasoning is permissible at the outer metamathematical layer? In principle, any kind of reasoning that would be allowed elsewhere in mathematics. The justification for such reasoning isn't different just because the subject matter is predicate calculus, instead of (say) number theory or group theory.
So now the question becomes one of formalization in general. This question has a couple of good answers. I would say briefly, formalization in ZFC became the "gold standard" of rigor during the 20th century. But on the one hand, much of math requires less than the full strength of ZFC. This is true for the examples in the fourth paragraph above. The subject matter is very concrete, just finite strings of symbols. At heart not much more is involved than plain old induction.
On the other hand, reasoning can be completely convincing, even rigorous, without being translated into the formalism of ZFC. Personally, if I saw a formal proof in ZFC of any of the examples above, it would not strengthen my belief in the truth of these results.