let t, u, v be GRZ-formula; :: thesis: ( t '=' u is LD-provable implies (t '&' v) '=' (u '&' v) is LD-provable )
assume A1: t '=' u is LD-provable ; :: thesis: (t '&' v) '=' (u '&' v) is LD-provable
(t '=' u) => ((t '&' v) '=' (u '&' v)) is LD-provable ;
hence (t '&' v) '=' (u '&' v) is LD-provable by A1, Th62; :: thesis: verum