bi.bldbi>

Theorem.

Arguments:

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

Hypotheses:

()

Assertions:

(()())

Proof:

Hyp	Ref	Line	Expr
	Hypo	1	()
	dfbi	2	(()(()()))
1	bi.bldim<	3	(()())
3	bi.bldan>	4	((()())(()()))
2, 4	bitr	5	(()(()()))
1	bi.bldim>	6	(()())
6	bi.bldan<	7	((()())(()()))
5, 7	bitr	8	(()(()()))
	dfbi	9	(()(()()))
8, 9	><bitr	10	(()())