eqt<

Theorem.

Arguments:

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

Assertions:

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

Proof:

Hyp Ref Line Expr
ax-tr1((xeqy)to((yeqz)to(xeqz)))
ax-tr2((yeqx)to((xeqz)to(yeqz)))
2ax-sym3((xeqy)to((xeqz)to(yeqz)))
1, 3>bid4((xeqy)to((xeqz)leftrightarrow(yeqz)))