Go backward to B.5.2 Quantifier Consequences Go up to B.5 Deriving New Knowledge

B.5.3 Substitutions

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

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.