Substitution of equals for equals

Anytime you have an equality hypothesis relating two terms, e.g.,

(equallhsrhs)

it is legal to substitute one for the other anyplace else in the formula. Doing so does not change the truth value of the formula.

You can use a *negated equality* this way *provided* it appears
in the conclusion. For example, it is ok to transform

(implies (true-listp x) (not (equal x 23)))

to

(implies (true-listp 23) (not (equal x 23)))

by substitutions of equals for equals. That is because, by *contrapositive* forms:

(implies (equal x 23) (not (true-listp x)))

and

(implies (equal x 23) (not (true-listp 23)))

and see the equality as a hypothesis and the substitution of

Sometimes people speak loosely and say ``substitution of equals for
equals'' when they really mean ``substitutions of equivalents for
equivalents.'' Equality, as tested by *provided* the target term occurs in a
propositional place, as discussed at the bottom of

Now use your browser's **Back Button** to return to the example proof in
logic-knowledge-taken-for-granted.