tr<

Theorem.

Arguments:

x (obj), y (obj), z (obj),

Assertions:

((xeqy)to((zeqx)to(zeqy)))

Proof:

Hyp Ref Line Expr
ax-tr1((zeqx)to((xeqy)to(zeqy)))
1com12i2((xeqy)to((zeqx)to(zeqy)))