### LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-EQUALS-FOR-EQUALS

substitution of equals for equals
Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

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

(equal *lhs* *rhs*)

it is legal to substitute one for the other anyplace else in the formula.
Doing so does not change the truthvalue 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
propositional calculus,
we could rearrange the formulas into their *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 `23`

for `x`

as
sensible.
Sometimes people speak loosely and say ``substitution of equals for equals''
when they really mean ``substitutions of equivalents for equivalents.''
Equality, as tested by `EQUAL`

, is only one example of an equivalence
relation. The next most common is propositional equivalence, as tested by
`IFF`

. You can use propositional equivalence hypotheses to substitute
one side for the other *provided* the target term occurs in a propositional
place, as discussed at the bottom of
propositional calculus.

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