Description: Lemma for axpr . Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023) (Proof shortened by Matthew House, 18-Sep-2025)