If you have a given of the form *x* = *y*, then in any given or
goal you may substitute *y* for *x* or *x* for *y*. To
perform such a substitution, select the given or goal in which you would
like to do the substitution, and position the mouse over the Substitute
command. A submenu will appear, listing all available substitutions; an
entry of the form “*x**y*” means “replace *x* by
*y*”. Select the substitution you would like to perform, and a
dialog box will open. The statement in which the substitution is to be
performed appears at the top of the dialog box, and initially the entire
statement is selected. You can perform the substitution in only part of
the statement by selecting the part in which you want the substitution to
be performed. Selecting works in the usual way, except that when you drag
the mouse across a part of the statement, what gets selected is *the
smallest meaningful subexpression containing the symbols you drag
across*. For example, if you drag the mouse across the symbols
“*x*” in the statement
“*x**A**y**B*”,
what will be selected is the statement “*x**A*”.

Click the Substitute button to perform the substitution. The other buttons in the dialog box can be used to rewrite the statement in some other ways; for details see the instructions for the Reexpress command.