eqtr

Theorem.

Arguments:

x (st), y (st), z (st),

Assertions:

((xeqy)to((yeqz)to(xeqz)))

Proof:

Hyp Ref Line Expr
ax81((yeqx)to((yeqz)to(xeqz)))
1eqcomi2((xeqy)to((yeqz)to(xeqz)))