Description: The general form of the *alrim* family of theorems: if ph is
substituted for ps , then the antecedent expresses a form of
nonfreeness of x in ph , so the theorem means that under a
nonfreeness condition in an antecedent, one can deduce from the
universally quantified implication an implication where the consequent is
universally quantified. Dual of bj-exlimg . (Contributed by BJ, 9-Dec-2023)