eqsym

Theorem.

Arguments:

a (obj), b (obj),

Assertions:

((aeqb)to(beqa))

Proof:

Hyp Ref Line Expr
df-equ1((aeqb)to((aleb)wedge(blea)))
1ancom2((aeqb)to((blea)wedge(aleb)))
df-equ3(((blea)wedge(aleb))to(beqa))
2, 3syl4((aeqb)to(beqa))