### B.5.3 Substitutions

The equality axioms and the properties of logical equivalence allow us to
draw the following conclusions.

**Proposition 157 (Substitutions)**
For all terms `S` and `T`, formulas `A` and
`B`, variables `x` and formula patterns `C` with
variable `F`, the following holds:
**Equality Subsitutions**-
`S`=`T` /\ `A`[`x` <- `S`] |

`A`[`x` <- `T`] |

**Equivalence Substitutions**-
`A` <=> `B` /\ `C`[`F` <- `A`] |

`C`[`F` <- `B`] |

The substitution laws allow us to replace in a goal "terms by
equal terms" and "formulas by equivalent formulas". These laws are applied
when we say

We have to prove `F`[`x` <- `T`].
Because `T`=`U`, it suffices to prove `F`[`x` <- `U`].

and thus reduce a problem to an equivalent subproblem.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999