(t '=' u) => ((t '&' v) '=' (u '&' v)) in LD-specific-axioms by Def11;
hence (t '=' u) => ((t '&' v) '=' (u '&' v)) is LD-axiomatic by XBOOLE_0:def 3; :: thesis: verum