Go backward to B.5.2 Quantifier Consequences
Go up to B.5 Deriving New Knowledge
The equality axioms and the properties of logical equivalence allow us to draw the following conclusions.
|S=T /\ A[x <- S]|
|A[x <- T]|
|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.