Description: Version of pm11.53v with nonfreeness antecedents. One can also prove the theorem with antecedent ( F// y A. x ph /\ A. y F// x ps ) . (Contributed by BJ, 7-Oct-2024)