Description: A version of spcdv where ps and ch are direct substitutions of each other. This theorem is useful because it does not require ph and x to be distinct variables. (Contributed by Emmett Weisz, 12-Apr-2020)