df<-alt3

Theorem.

Arguments:

(obj), (obj),

Assertions:

(()(()()))

Proof:

Hyp	Ref	Line	Expr
	df<-alt2	1	(()(()()))
	df-equ	2	(()(()()))
2	bi.bldneg	3	(()(()()))
3	bi.bldan>	4	((()())(()(()())))
	banc<	5	((()())(()(()())))
	im.an	6	((()())(()()))
	im.an	7	((()(()()))(()(()())))
5, 6, 7	>2bitr	8	((()())(()(()())))
8	conb	9	((()())(()(()())))
1, 4, 9	<2bitr	10	(()(()()))