aleqcom

Theorem.

Arguments:

(sv), (sv),

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	ax10	1	(()(()()))
1	imabs	2	(()())
	eqcomi	3	(()())
3	im.bldal	4	(()())
2, 4	syl	5	(()())