eqsym
Theorem.
Arguments:
(obj),
(obj),
Assertions:
((
)
(
))
Proof:
Hyp
Ref
Line
Expr
df-equ
1
((
)
((
)
(
)))
1
ancom
2
((
)
((
)
(
)))
df-equ
3
(((
)
(
))
(
))
2, 3
syl
4
((
)
(
))