### 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.