Description: Inference associated with exlimi . Inferring a theorem when it is implied by an antecedent which may be true. (Contributed by BJ, 15-Sep-2018)