theorem Th74: :: GRZLOG_1:27

for t, u, v being GRZ-formula st t '=' u is LD-provable & u '=' v is LD-provable holds
t '=' v is LD-provable