eqt>

Theorem.

Arguments:

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

Assertions:

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

Proof:

Hyp Ref Line Expr
com1((xeqz)leftrightarrow(zeqx))
com2((yeqz)leftrightarrow(zeqy))
1, 2bi.bldbi<>3(((xeqz)leftrightarrow(yeqz))leftrightarrow((zeqx)leftrightarrow(zeqy)))
eqt<4((xeqy)to((xeqz)leftrightarrow(yeqz)))
3, 4brpi225((xeqy)to((zeqx)leftrightarrow(zeqy)))