|Description: This theorem can be used
to eliminate a distinct variable restriction on
and and replace it with the
as an antecedent. normally has free and can be read
substitutes for and can be read
. We do not require that and be
they are not, the distinctor will become false (in multiple-element
domains of discourse) and "protect" the consequent.
To obtain a closed-theorem form of this inference, prefix the hypotheses
with , conjoin them, and apply dvelimdf 2133.
Other variants of this theorem are dvelimh 2134 (with no distinct variable
restrictions) and dvelimhw 2013 (that avoids ax-13 2055). (Contributed by