com

Theorem.

Arguments:

x (obj), y (obj),

Assertions:

((xeqy)leftrightarrow(yeqx))

Proof:

Hyp Ref Line Expr
ax-sym1((xeqy)to(yeqx))
ax-sym2((yeqx)to(xeqy))
1, 2>bii3((xeqy)leftrightarrow(yeqx))