eqtr

Theorem.

Arguments:

(obj), (obj), (obj),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	df-equ	1	(()(()()))
1	siman<	2	(()())
	df-equ	3	(()(()()))
3	siman<	4	(()())
2, 4	im.bldan<>	5	((()())(()()))
5	tr-an	6	((()())())
1	siman>	7	(()())
3	siman>	8	(()())
7, 8	im.bldan<>	9	((()())(()()))
9	ancom	10	((()())(()()))
10	tr-an	11	((()())())
6, 11	jca	12	((()())(()()))
12	df-equ	13	((()())())
13	exp	14	(()(()()))