In proof theory, a proof system as the one presented in Ebbinghaus at al.'s book must find a balance between at least two features:
It should be handy to use to derive valid formulas; let us call this feature object manageability.
It should be handy to use to derive properties of the proof system itself and its derivations; let us call this feature meta-manageability.
Unfortunately, the two features may be in conflict with each other. The following is a schematic and slightly superficial representation of the issue, but it is helpful to give you an idea.
On the one side, object manageability would tend to add as many inference rules as possible. Indeed, if we can choose among many inference rules, such as $\land$ introduction, excluded middle, contraposition, explosion, chain syllogism, disjunctive syllogism, substitution, transitivity, etc., we have many tools to find a formal derivation of a valid formula $A$, and likely this derivation would be a natural formalization of our intuitive way to prove $A$. The more rules the proof system has, the handier the proof system is to find a derivation of a valid formula.
On the other side, meta-manageability would tend to add as few inference rules as possible. Indeed, when you want to prove a property of the proof system, if the proof system is made of few rules then it is easier to check such a property. For instance, a typical desired property of a proof system is soundness: the proof system can derive only valid formulas (tautologies, in propositional logic). To prove soundness, you essentially have to show that validity is preserved by each inference rule of the proof system: for each inference rule, if its premises are valid formulas, then its conclusion is also a valid formula too. Of course, the proof of soundness is easier if there are few inference rules to check.
How can we find a synthesis between object manageability and meta-manageability? A possible balance is given by the approach somehow followed by Ebbinghaus too.
First, let us fix our proof system as small as possible, in the sense that it contains as few inference rules as possible (anyway, the proof system cannot be minimized too much because it has to be complete, i.e. strong enough to be able to derive all valid formulas). These rules may seem clumsy to use, never mind, the important thing is that they are few in number. This way, meta-manageability is assured. Let us call these inference rules the core rules. In Ebbanghaus's proof system, the core rules are Ass, Ant, PC, Ctr, $\lor$A, $\lor$S.
Second, to ensure object manageability, let us prove that many other inference rules are derivable in the proof system. An inference rule with premises $P_1, \dots, P_n$ and conclusion $C$ is derivable if there is a derivation with hypotheses $P_1, \dots, P_n$ and conclusion $C$ that only uses the core rules of the proof system. These derivable rules such as $\land$ introduction, excluded middle, contraposition, explosion, chain syllogism, disjunctive syllogism, substitution, transitivity, etc., make the task of finding a derivation for a valid formula much easier, in the sense they are closer to our intuitive reasoning. But each of them is just a "macro" for a chain of core rules. You can freely use the derivable rules to derive a valid formula, but the properties of the proof system are "encapsulated" in the core rules.
For practical purposes, there is not a definitive answer to the question "How to approach the proof that an inference rule is derivable?", given a set of core inference rules. In particular, this is true for the core rules of Ebbinghaus' proof system, which are really clumsy (in the "First digression" section here you can find a brief discussion). Being able to use the given inference rules in a smart way, is a matter of practice. In general, the absence of a definitive answer to your question is the reason why proving something is a difficult task!
Since Ebbinghaus' core rules are really clumsy, my suggestion is the following: as soon as you want to use an inference scheme that seems to be natural and general enough, check if it derivable. In this way, in your next derivations you can use this derivable inference rule instead of a clumsy chain of core rules.
For instance, are you able to prove that the following (and very handy) inference rule is derivable in Ebbinghaus' system?
\begin{align}
\Gamma \vdash A
\\
\Gamma, \, A \vdash B
\\
\hline
\Gamma \vdash B
\end{align}
Best Answer
There is a very comprehensive (at least very long!) "Handbook of Mathematical Discourse" which you can find here.
Under the various topics they list some synonyms, but I can't vouch for its completeness or accuracy. Also, it is more of a dictionary or encyclopedia than a pure thesaurus.
EDIT: Another question on Math.SE asks a similar question and one of the answers points to this online encyclopedia. It seems, however, that this one might be of limited use as a thesaurus. After a few tries it looks like synonyms are rarely included.