nfv with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd. (Contributed by Mario Carneiro, 6-Oct-2016.)