anass

Theorem.

Arguments:

(pr), (pr), (pr),

Assertions:

((())(()))

Proof:

Hyp	Ref	Line	Expr
	impexp	1	((())(()))
	im.nan	2	(()())
2	bi.bldim>	3	((())(()))
1, 3	bitr	4	((())(()))
4	bi.bldneg	5	((())(()))
	df-an	6	((())(()))
	df-an	7	((())(()))
5, 6, 7	<2bitr	8	((())(()))