equational calculus

[gusl]

I am playing with an equational calculus.


Substitution rule:

EQN1 EQN2
---------------------- , for any VAR in both EQN1 and EQN2
SUBS(VAR, EQN1, EQN2)

(Note that SUBS(VAR, EQN1, EQN2) is free from VAR. So the choice of VAR may be important when there are several variables that appear in both EQN1 and EQN2)


SUBS(var, EQN1, EQN2) solves EQN2 for VAR, providing a substitution for VAR. This substitution is carried out on EQN1, and this is what SUBS returns.


Now I want to prove that:
Given any triple EQN1, EQN2, SUBS(VAR, EQN1, EQN2) (i.e. any triple where the third equation is derivable by the first two), any set with two equations from the above can derive the remaining equation. That is,
EQN1, SUBS(VAR, EQN1, EQN2) |- EQN2 and EQN2, SUBS(VAR, EQN1, EQN2) |- EQN1

...but I have no idea how.