A Rich Theory is one whose axioms (expressed in 1st order logic) contain a large number of predicates and functors, and whose theorems are often provable from a subset of the axioms. Experimental results have shown that the removal of just a few unnecessary axioms can have a significant effect on the performance of an ATP system on a problem. This work introduces a relevance measure that estimates the potential usefulness of an axiom for proving a given theorem. The measure has been used in a control algorithm that selects combinations of axioms based on their relevance, to form {\em axiom reduced} problems that are submitted to an ATP system. Evaluation shows that this system performs better than the ATP system alone. Additionally, a scheme for using the relevance measures for selecting lemmas to augment the axioms of a problem is introduced.