Logical equivalence in BV

Dear all,
I just noticed a curious thing about BV: logical equivalence seems to
correspond exactly to structural congruence. More formally,
here's the conjecture:

R and T are "syntactically" equivalent if and only if both [R, -T]
and [-R, T] are provable.

Is this something known already?

-Alwen