Description: Inference associated with 19.23 . See exlimiv for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993) (Revised by Mario Carneiro, 24-Sep-2016)